proposition: Lemma limitb_limit alpha : limitb alpha -> Omega_limit (canon alpha) alpha.
proof: Proof. destruct alpha; inversion 1. destruct n; [discriminate | unfold canon]. split; destruct n0; try discriminate. - left; auto with arith. - destruct y; inversion_clear 1. exists (S n1). assert( H0: (n0 = n \/ n0 < n)%nat) by lia. destruct H0. + subst; right; auto. + left; auto. + abstract lia. Qed.
imports: Coq(Arith Compare_dec Lia) hydras(Simple_LexProd ON_Generic ON_mult ON_Omega Compat815)