proposition: Lemma eq_equiv : Equivalence eq.
proof: Proof. split; intro; intros. reflexivity. symmetry. assumption. etransitivity; eassumption. Qed.
imports: MSets Arith NArith Notations Sorting Coq.Program.Equality GeoCoq.Tactics.Coinc.tactics_axioms