proposition: Lemma lt_succ alpha : alpha o< succ alpha.
proof: Proof. destruct alpha; simpl; constructor; abstract lia. Qed.
imports: Coq(Arith Compare_dec Lia) hydras(Comparable Simple_LexProd ON_Generic ON_plus ON_Omega Compat815)