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. + apply le_introl. abstract lia. - inversion_clear 1. inversion_clear H0. constructor; abstract lia. constructor; auto with arith. - split. simpl. constructor. + constructor. + constructor. - split. inversion_clear 1. inversion_clear 1. inversion H0. - split. inversion_clear 1. simpl. apply le_intror. abstract lia. simpl. inversion_clear 1. inversion_clear H0; constructor;abstract lia. constructor;abstract lia. Qed.
imports: Coq(Arith Compare_dec Lia) hydras(Comparable Simple_LexProd ON_Generic ON_plus ON_Omega Compat815)