proposition: Lemma Canon_mono1 alpha i j : E0limit alpha -> (i< j)% nat -> (Canon alpha i o< Canon alpha j)%e0.
proof: Proof. destruct alpha. unfold Canon. destruct i, j. - inversion 2. - unfold lt. simpl. intros. clear H0. split; auto. cbn. auto with T1. now apply nf_canon. split; cbn. specialize (T1limit_canonS_not_zero j cnf_ok H). intro. apply canon_limit_mono; auto. auto with arith. apply nf_canon; auto. - intros; lia. - unfold lt; simpl. simpl; intros. apply canonS_limit_mono; auto. auto with arith. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)