proposition: Lemma lex_Opp: forall u v u' v', u = CompOpp u' -> v = CompOpp v' -> lex u v = CompOpp (lex u' v').
proof: Proof. intros ? ? u' ? -> ->. case u'; reflexivity. Qed.
imports: Bool PeanoNat BinPos Orders OrdersEx MSetInterface