proposition: Lemma divdec : forall n d : nat, divide d n \/ ~ divide d n.
proof: Proof. intros. assert (d = 0 \/ 0 < d) by lia. destruct H. + destruct n. - left. exists 0. auto. - right. intro. destruct H0. lia. + revert d H. apply (lt_wf_ind n). clear n. intros. assert (n = 0 \/ 0 < n) by lia. destruct H1. - left. exists 0. lia. - assert (d <= n \/ n < d) by lia. destruct H2. * assert (n - d < n) by lia. destruct (H _ H3 _ H0). ++ destruct H4. left. exists (S x). lia. ++ right. intro. apply H4. destruct H5. exists (x - 1). nia. * right. intro. destruct H3. destruct x; lia. Qed.
imports: Arith Wf_nat ZArith Peano_dec ZArith_dec NatAux ZCAux ZCmisc ZSum Pmod Ppow