proposition: Lemma L_spec1 (a:T1) (f:nat -> nat) : a != zero -> L_spec a f <-> (forall k, Large_Sets.mlarge (g2h a) ( MoreLists.interval (S k) (Nat.pred (f (S k))))) .
proof: Proof. move => Ha. have Hdiff : a <> zero. move => H0; subst. by cbn in Ha. rewrite /L_spec; split => H. inversion H as [f0 H0 H1 H2| a0 f0 H0 H1 H2 H3]. { suff Hzero: a = zero by contradiction. apply g2h_eqE. by rewrite -H1. } move => k; move: (H1 k). rewrite interval_def => //. right; move => Hzero //. apply Hdiff; apply g2h_eqE; by rewrite Hzero. Qed.
imports: mathcomp(all_ssreflect zify) Coq(Logic.Eqdep_dec) hydras(DecPreOrder) hydras(T1 E0) hydras(L_alpha) gaia_hydras(T1Bridge GCanon GPaths GHprime)