proposition: Lemma limit_canonS_not_zero i lambda: T1nf lambda -> T1limit lambda -> canon lambda i.+1 <> zero.
proof: Proof. rewrite -(h2g_g2hK lambda) /canon => Hnf Hlim . change zero with (h2g T1.zero); rewrite h2g_eqE. apply Canon.T1limit_canonS_not_zero. - move: Hnf; by rewrite g2h_h2gK -nf_ref. - by rewrite T1limit_ref h2g_g2hK. Qed.
imports: mathcomp(all_ssreflect zify) hydras(Canon) T1Bridge hydras(T1) gaia(ssete9)