proposition: Lemma canonS_zero_inv (alpha:T1) (i:nat) : canon alpha (S i) = zero -> alpha = zero \/ alpha = one.
proof: Proof. destruct alpha; cbn; auto. destruct alpha1, n, alpha2;auto; try discriminate. all: destruct (T1.pred (cons alpha1_1 n0 alpha1_2)); try discriminate. Qed.
imports: hydras.Prelude(DecPreOrder)