proposition: Lemma le_lt_trans : forall p q r, p o<= q -> q o< r -> p o< r.
proof: Proof. destruct 1; trivial. intro; now transitivity y. Qed.
imports: Coq(Arith Compare_dec Lia) hydras(Comparable Simple_LexProd ON_Generic ON_plus ON_Omega Compat815)