proposition: Lemma le_intror : forall i j k:nat, (j <= k)%nat -> (i,j) o<= (i,k).
proof: Proof. intros i j k H; destruct (Compat815.le_lt_or_eq j k H). - left; now constructor 2. - subst k; now right. Qed.
imports: Coq(Arith Compare_dec Lia) hydras(Simple_LexProd ON_Generic ON_mult ON_Omega Compat815)