proposition: Theorem le_2_n_pred : forall (n:nat)(h: 2 <= n), pred_partial n (le_2_n_not_zero n h) <> 0.
proof: Proof. Abort. Theorem le_2_n_pred' : forall n:nat, 2 <= n -> forall h:n <> 0, pred_partial n h <> 0. Proof. intros n Hle; elim Hle. intros; discriminate. simpl; intros; apply le_2_n_not_zero; assumption. Qed.
imports: ZArith List Arith Lia Zwf