proposition: Lemma standard_gnaw_iota_from i a l : i <> 0 -> standard_gnaw i a l = gnaw a (iota i l).
proof: Proof. move: l i a; elim => // /=. rewrite !/standard_gnaw => n Hn i a Hi. move: (Hn (S i) (canon a i)); rewrite /canon g2h_h2gK. move => {}Hn; rewrite Hn /gnaw ?g2h_h2gK => // /=; by case :i Hn Hi. Qed.
imports: mathcomp(all_ssreflect zify) hydras(Canon Paths) gaia_hydras(T1Bridge GCanon) hydras(T1) gaia(ssete9)