proposition: Lemma beq_nat_ok : forall n1 n2, if Nat.eqb n1 n2 then n1 = n2 else n1 <> n2.
proof: Proof. intros n1 n2; destruct (Nat.eqb n1 n2) eqn:E. - exact (proj1 (Nat.eqb_eq n1 n2) E). - exact (proj1 (Nat.eqb_neq n1 n2) E). Defined.
imports: Coq(Relation_Definitions Setoid Bool Arith)