I am learning Coq with ssreflect. Just to understand things, I've proved
forall a b : bool, a == b -> a = b but I can't figure out how to prove
forall m n : nat, m == n -> m = n. I've tried using the
elim tactic first on
m, then on
n, but in the end I was left with a subgoal I couldn't prove. I've tried
destruct m and then
destruct n but the result was the same.
A minimal working example to try to prove this is
From mathcomp Require Import all_ssreflect. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. Lemma eqn_impl_eq (m n : nat) (m_eqn_n : is_true (m == n)) : m = n. Proof. Admitted.
It uses mathcomp library though.