proposition: Lemma E0_pred_Lt (alpha : E0) : alpha <> E0zero -> E0limit alpha = false -> E0_pred alpha o< alpha.
proof: Proof. unfold E0limit, E0_pred, E0lt; destruct alpha; intros. simpl. destruct (T1.zero_limit_succ_dec cnf_ok0 ). destruct s. - subst. unfold E0zero in H. destruct H. f_equal;apply nf_proof_unicity. - simpl in H0; rewrite i in H0; discriminate. - destruct s. destruct a. simpl. subst cnf0. apply LT_succ;auto. 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)