proposition: Lemma nat_compare_lt_gt_sym: forall n m, Nat.compare n m = Lt <-> Nat.compare m n = Gt.
proof: Proof. intros;split;intros. apply nat_compare_lt in H. rewrite lt_gt in H. rewrite <- nat_compare_gt;trivial. apply nat_compare_gt in H. rewrite <- lt_gt in H. rewrite <- nat_compare_lt;trivial. Qed.
imports: Coq(List) Coq(Arith)