proposition: Lemma E0_pred_succK x : E0_pred (E0_succ x) = x.
proof: Proof. apply E0_eqE; rewrite /E0_pred. apply E0_eq_intro => //=. rewrite pred_succ => //. case: x => c Hc //=. by apply /eqP. Qed.
imports: mathcomp(all_ssreflect zify) Coq(Logic.Eqdep_dec) hydras(DecPreOrder ON_Generic T1 E0)