proposition: Lemma L_pos_inv a f : a != zero -> L_spec a f -> forall k, (S k < f (S k))%N.
proof: Proof. move => Ha H k. have Hdiff : a <> zero. move => H0; subst. by cbn in Ha. apply /ltP; apply Large_Sets.L_pos_inv with (g2h a) => //. move => H0; apply Hdiff,g2h_eqE, H0. Qed.
imports: mathcomp(all_ssreflect zify) Coq(Logic.Eqdep_dec) hydras(DecPreOrder) hydras(T1 E0) hydras(L_alpha) gaia_hydras(T1Bridge GCanon GPaths GHprime)