proposition: Lemma canon_limit_mono lambda i j (Hnf : T1nf lambda) (Hlim : T1limit lambda) (Hij : (i < j)%N) : canon lambda i < canon lambda j.
proof: Proof. rewrite /canon -hlt_iff. case (@canon_limit_mono (g2h lambda) i j) => //. - by rewrite hnf_g2h. - by rewrite T1limit_ref h2g_g2hK. - by apply /ltP . - move => _; case => //. Qed.
imports: mathcomp(all_ssreflect zify) hydras(Canon) T1Bridge hydras(T1) gaia(ssete9)