proposition: Lemma Lt_Succ_Le (alpha beta: E0): beta o< alpha -> E0_succ beta o<= alpha.
proof: Proof. destruct alpha, beta;simpl in *. unfold leq, E0lt; simpl. intro; rewrite Le_iff; split; auto. - apply T1.succ_nf; auto. - split; auto. + apply T1.lt_succ_le;auto. destruct H; tauto. Qed.
imports: Coq(Arith Max Bool Lia Compare_dec Relations Ensembles ArithRing Wellfounded Operators_Properties Logic.Eqdep_dec) hydras(Prelude.More_Arith Prelude.Restriction Prelude.DecPreOrder ON_Generic OrdNotations)