proposition: Lemma le_0 : forall p: t, fin 0 o<= p.
proof: Proof. destruct p. destruct n ; [right |]. constructor. constructor. auto with arith. left; constructor. Qed.
imports: Coq(Arith Compare_dec Lia) hydras(Comparable Simple_LexProd ON_Generic ON_plus ON_Omega Compat815)