proposition: Theorem LT_to_standard_path (a b : T1) : T1nf a -> T1nf b -> b < a -> {n : nat & {j:nat | standard_path n.+1 a j b}}.
proof: Proof. rewrite -!hnf_g2h => nfa nfb Hlt. case (@LT_to_standard_path (g2h a) (g2h b)). rewrite -T1lt_iff -?hnf_g2h => //. move => x; case => j Hj; exists x, j; by rewrite /standard_path. Qed.
imports: mathcomp(all_ssreflect zify) hydras(Canon Paths) gaia_hydras(T1Bridge GCanon) hydras(T1) gaia(ssete9)