proposition: Lemma canonS_cons_not_zero : forall i alpha n beta, alpha <> zero -> canon (cons alpha n beta) (S i) <> zero.
proof: Proof. destruct alpha. - now destruct 1. - intros; cbn. destruct n0, beta, alpha1, n; try discriminate. all: destruct (T1.pred alpha2); try discriminate. Qed.
imports: hydras.Prelude(DecPreOrder)