proposition: Lemma path_to_LT b s a: path_to b s a -> T1nf a -> T1nf b -> b < a.
proof: Proof. rewrite -!hnf_g2h /path_to => Hpath Ha Hb. move: (path_to_LT Hpath Ha); rewrite T1lt_iff => //; by rewrite -hnf_g2h. Qed.
imports: mathcomp(all_ssreflect zify) hydras(Canon Paths) gaia_hydras(T1Bridge GCanon) hydras(T1) gaia(ssete9)