proposition: Lemma lt_succ_le alpha beta : alpha o< beta <-> succ alpha o<= beta.
proof: Proof. destruct alpha, beta. unfold succ; cbn. split. - inversion_clear 1. + left; now left. + now apply le_intror. - intros; eapply lt_le_trans . instantiate (1 := (n, S n0)). right; auto. assumption. Qed.
imports: Coq(Arith Compare_dec Lia) hydras(Simple_LexProd ON_Generic ON_mult ON_Omega Compat815)