proposition: Lemma canon_tail a (n : nat) b (i : nat): T1nf (cons a n b) -> b <> zero -> canon (cons a n b) i = cons a n (canon b i).
proof: Proof. move => Hnf Hpos; rewrite -g2h_eqE g2h_canon !g2h_cons g2h_canon canon_tail //. move: Hnf; rewrite -hnf_g2h !g2h_cons => //. move: b {Hnf} Hpos ; by case. Qed.
imports: mathcomp(all_ssreflect zify) hydras(Canon) T1Bridge hydras(T1) gaia(ssete9)