proposition: Lemma compare_reflect_eq: forall u v, compare u v = Eq -> eval u == eval v.
proof: Proof. intros u v. case (tcompare_weak_spec u v); intros; try congruence. reflexivity. Qed.
imports: Coq(Arith NArith List) Coq(FMapPositive Relations RelationClasses) AAC_tactics(Utils Constants)