proposition: Lemma E0_pred_of_Succ (alpha:E0) : E0_pred (E0_succ alpha) = alpha.
proof: Proof. unfold E0_pred; destruct (Zero_Limit_Succ_dec (E0_succ alpha)). destruct s. - unfold E0_succ, E0zero in e; injection e . intro H; now destruct (T1.succ_not_zero (cnf alpha)). - unfold T1limit, E0_succ in e; simpl in e; destruct (@T1.T1limit_succ (cnf alpha)); auto. destruct alpha; simpl; auto. - destruct s. { unfold E0_succ in e; injection e. destruct alpha, x;simpl; intros; apply T1.succ_injective in H; auto. - subst; replace cnf_ok1 with cnf_ok0; trivial. eapply nf_proof_unicity. } 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)