proposition: Lemma T1add_not_monotonous_l : exists a b c : T1, a t1< b /\ a + c = b + c.
proof: Proof. exists 3, 5, T1omega; now compute. Qed.
imports: Coq(Arith Max Bool Lia Compare_dec Relations Ensembles Wellfounded Bool RelationClasses Operators_Properties ArithRing Logic.Eqdep_dec) hydras(More_Arith Restriction DecPreOrder) hydras(OrdNotations)