proposition: Lemma cmp_opp f g : cmp f g = CompOpp (cmp g f).
proof: Proof. destruct f; destruct g; try refl. apply Ty_Cmp.cmp_opp. Qed.
imports: CoLoR(LogicUtil OrdUtil LSimple RelUtil) Coq(Structures.Equalities Lia) Coq(Compare_dec)