proposition: Lemma canonS_LE alpha n : nf alpha -> canon alpha (S n) t1<= canon alpha (S (S n)).
proof: Proof. intro H; destruct (zero_limit_succ_dec H). - destruct s. + subst; cbn. apply LE_refl; auto with T1. + apply LE_r; eapply canonS_limit_mono; auto. - destruct s as [gamma [Hgamma Hgamma']]; subst . repeat rewrite canon_succ;auto with T1. apply LE_refl;auto. Qed.
imports: hydras.Prelude(DecPreOrder)