proposition: Lemma nat_compare_case : forall (n1 n2:nat), (lt n1 n2) \/ (n1=n2) \/ (lt n2 n1).
proof: Proof. induction n1. destruct n2. tauto. left. auto with arith. destruct n2. right. right. auto with arith. elim (IHn1 n2). intro. left. auto with arith. intro. elim H. intro. right. left. auto. intro. right. right. auto with arith. Qed.
imports: Arith Coq.Logic.Eqdep_dec Coq.Arith.Peano_dec List Recdef