proposition: Lemma canonS_lt (i : nat) [a : T1]: T1nf a -> a <> zero -> T1lt (canon a i.+1) a.
proof: Proof. rewrite -(h2g_g2hK a) -nf_ref /canon => Hnf Hpos. rewrite g2h_h2gK; apply lt_ref, Canon.canon_lt => //. move => H; apply Hpos; rewrite H => //. Qed.
imports: mathcomp(all_ssreflect zify) hydras(Canon) T1Bridge hydras(T1) gaia(ssete9)