proposition: Lemma Cor12 (a: T1) : T1nf a -> forall b i n, T1nf b -> b < a -> (i < n)%N -> const_path i.+1 a b -> const_path n.+1 a b.
proof: Proof. rewrite -hnf_g2h => Hnf b i n Hb Hlt Hij; apply Cor12 => //. rewrite -T1lt_iff => //; by rewrite -hnf_g2h. by apply /ltP. Qed.
imports: mathcomp(all_ssreflect zify) hydras(Canon Paths) gaia_hydras(T1Bridge GCanon) hydras(T1) gaia(ssete9)