proposition: Lemma le_0 : forall p: t, (0,0) o<= p.
proof: Proof. destruct p, n ; auto. - apply le_intror; lia. - left; left; lia. Qed.
imports: Coq(Arith Compare_dec Lia) hydras(Simple_LexProd ON_Generic ON_mult ON_Omega Compat815)