proposition: Lemma nat_compare_eq_sym: forall n m, Nat.compare n m = Eq <-> Nat.compare m n = Eq.
proof: Proof. intros;split;intros;rewrite nat_compare_Eq;rewrite nat_compare_Eq in H;symmetry;trivial. Qed.
imports: Coq(List) Coq(Arith)