proposition: Lemma path_to_inv1 to i from : path_to to [:: i] from -> i <> 0 /\ transition i from to.
proof: Proof. inversion 1. split; trivial. move: H2; rewrite /transition; rewrite /htransition. destruct i. contradiction. rewrite /transition_S. destruct 1. repeat split. destruct from. destruct H4. by []. by []. rewrite /canon. apply /eqP. by rewrite -g2h_eqE g2h_h2gK. split; trivial. inversion H5. Qed.
imports: mathcomp(all_ssreflect zify) hydras(Canon Paths) gaia_hydras(T1Bridge GCanon) hydras(T1) gaia(ssete9)