proposition: Lemma canon_lt (i : nat) [a : T1]: T1nf a -> a <> zero -> canon a i < a.
proof: Proof. case: i => [| n Hnf Hpos]. - apply canon0_lt. - apply canonS_lt => //. Qed.
imports: mathcomp(all_ssreflect zify) hydras(Canon) T1Bridge hydras(T1) gaia(ssete9)