proposition: Lemma H'_omega k : H'_ E0_omega k = (2 * k).+1 %nat.
proof: Proof. rewrite H'_eq3 ?/E0limit => //. replace (E0Canon E0_omega k.+1) with (E0fin k.+1); last first. apply gE0_eq_intro => /=; by rewrite E0fin_cnf T1succ_nat. rewrite /H'_ E0g2h_Fin H'_Fin; lia. Qed.
imports: mathcomp(all_ssreflect zify) Coq(Logic.Eqdep_dec) hydras(DecPreOrder T1 E0) hydras(Iterates Hprime L_alpha) gaia_hydras(T1Bridge GCanon GPaths)