proposition: Lemma H'_eq1 (i: nat) : H'_ E0zero i = i.
proof: Proof. by rewrite /H'_ g2h_E0zero Epsilon0.Hprime.H'_eq1. Qed.
imports: mathcomp(all_ssreflect zify) Coq(Logic.Eqdep_dec) hydras(DecPreOrder T1 E0) hydras(Iterates Hprime L_alpha) gaia_hydras(T1Bridge GCanon GPaths)