proposition: Lemma gcanon_limit_v2 (lambda: T1): T1nf lambda -> T1limit lambda -> limit_v2 (canon lambda) lambda.
proof: Proof. move => Hnf Hlim; split. - move => n; apply canon_lt => // H; subst; discriminate. - move => y Hnfy Hlt; case (canon_limit_strong Hnf Hlim Hnfy Hlt) => //. move => i Hi; exists i => //; by apply T1ltW. Qed.
imports: mathcomp(all_ssreflect zify) hydras(Canon) T1Bridge hydras(T1) gaia(ssete9)