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