proposition: Lemma path_to_iff1 to i from : T1nf from -> i <> 0 -> from <> zero -> path_to to [:: i] from <-> to = canon from i /\ T1nf from.
proof: Proof. move => H H0 H1 ; split; rewrite /path_to. move => H2; case (path_to_inv1 _ _ _ H2) => {}H2 H3. case: H3; repeat split => //; by apply /eqP. constructor => //. destruct i => //. case: H2 => H2 H3; constructor. move => H4; apply H1; by rewrite -g2h_eqE. move: H2; rewrite -g2h_eqE ; by rewrite -g2h_canon. Qed.
imports: mathcomp(all_ssreflect zify) hydras(Canon Paths) gaia_hydras(T1Bridge GCanon) hydras(T1) gaia(ssete9)