proposition: Lemma nat_compare_Eq: forall n m, Nat.compare n m = Eq <-> n = m.
proof: Proof. induction n. split; intros. apply nat_compare_eq; trivial. unfold Nat.compare. destruct m; trivial. discriminate H. intros. split. intros. apply nat_compare_eq; trivial. intros. destruct m. discriminate H. inversion H. generalize H1; intro. apply IHn in H1. unfold Nat.compare. subst. destruct m; trivial. Qed.
imports: Coq(List) Coq(Arith)