proposition: Lemma eq_nat_correct : forall n m, n<>m -> false=Nat.eqb n m.
proof: Proof. intros n. induction n. destruct m. intros. contradiction H. reflexivity. intros. compute. reflexivity. induction m. compute. reflexivity. simpl. intros. apply IHn. auto with arith. Qed.
imports: Coq(Arith Euclid Compare Lia)