proposition: Lemma canonS_zero_inv (a : T1) (i : nat): canon a i.+1 = zero -> a = zero \/ a = one.
proof: Proof. move => Ha; have H: hcanon (g2h a) i.+1 = T1.zero; last first. case (Canon.canonS_zero_inv (g2h a) i) => // H0 ; [left | right]; rewrite -(h2g_g2hK a) H0 //. move: Ha;change zero with (h2g T1.zero); by rewrite h2g_eqE. Qed.
imports: mathcomp(all_ssreflect zify) hydras(Canon) T1Bridge hydras(T1) gaia(ssete9)