proposition: Lemma LT_path_to (a b : T1) : T1nf a -> T1nf b -> b < a -> {s : list nat | path_to b s a}.
proof: Proof. move => Ha Hb Hlt; generalize (@LT_path_to (g2h a) (g2h b)) => H. rewrite /path_to; apply H, T1lt_iff => //. Qed.
imports: mathcomp(all_ssreflect zify) hydras(Canon Paths) gaia_hydras(T1Bridge GCanon) hydras(T1) gaia(ssete9)