proposition: Lemma Lemma2_6_1 (a:T1) : T1nf a -> forall b, T1nf b -> b < a -> {n:nat | const_path n.+1 a b}.
proof: Proof. rewrite -hnf_g2h => Hnf b Hb Hlt. have H: T1.nf (g2h b) by rewrite hnf_g2h. have H'lt : g2h b t1< g2h a; repeat split => //. move: Hlt; rewrite T1lt_iff => //. case => ? [? ?] //. by rewrite -hnf_g2h. case (Lemma2_6_1 Hnf H'lt) => x Hx; exists x. by rewrite /const_pathS. Qed.
imports: mathcomp(all_ssreflect zify) hydras(Canon Paths) gaia_hydras(T1Bridge GCanon) hydras(T1) gaia(ssete9)