proposition: Lemma canon_limit_of lambda (Hnf : T1nf lambda) (Hlim : T1limit lambda) : limit_of (canon lambda) lambda.
proof: Proof. split => // [n m Hnm|]; [apply canon_limit_mono | apply gcanon_limit_v2]; done. Qed.
imports: mathcomp(all_ssreflect zify) hydras(Canon) T1Bridge hydras(T1) gaia(ssete9)