proposition: Lemma constant_to_standard_path (a b : T1) (i : nat): T1nf a -> const_path i.+1 a b -> zero < a -> {j:nat | standard_path i.+1 a j b}.
proof: Proof. rewrite -hnf_g2h => nfa Hpath Hpos. case (@constant_to_standard_path (g2h a) (g2h b) i) => //. move: Hpos; rewrite T1lt_iff -?hnf_g2h => //. move => x Hx; exists x; by rewrite /standard_path. Qed.
imports: mathcomp(all_ssreflect zify) hydras(Canon Paths) gaia_hydras(T1Bridge GCanon) hydras(T1) gaia(ssete9)