proposition: Theorem H'_L_ a i: (H'_ a i <= L_ a i.+1)%N.
proof: Proof. rewrite /L_ /H'_; apply /leP; by apply L_alpha.H'_L_. Qed.
imports: mathcomp(all_ssreflect zify) Coq(Logic.Eqdep_dec) hydras(DecPreOrder) hydras(T1 E0) hydras(L_alpha) gaia_hydras(T1Bridge GCanon GPaths GHprime)