proposition: Lemma L_ge_S alpha i: alpha <> E0zero -> (i < L_ alpha i)%N.
proof: Proof. move => Halpha. rewrite /L_; apply /ltP. apply L_alpha.L_ge_S. move => H; apply Halpha, E0_eqE => //. rewrite H; by apply E0_eq_intro. Qed.
imports: mathcomp(all_ssreflect zify) Coq(Logic.Eqdep_dec) hydras(DecPreOrder) hydras(T1 E0) hydras(L_alpha) gaia_hydras(T1Bridge GCanon GPaths GHprime)