proposition: Lemma canonS_LE a n: T1nf a -> canon a n.+1 <= canon a n.+2.
proof: Proof. rewrite -(h2g_g2hK a) -nf_ref /canon g2h_h2gK => Hnf; by apply le_ref, canonS_LE. Qed.
imports: mathcomp(all_ssreflect zify) hydras(Canon) T1Bridge hydras(T1) gaia(ssete9)