proposition: Lemma div_plus_r : forall a b d : nat, divide d a -> divide d (a + b) -> divide d b.
proof: Proof. intros. destruct H, H0. exists (x0 - x). nia. Qed.
imports: Arith Wf_nat ZArith Peano_dec ZArith_dec NatAux ZCAux ZCmisc ZSum Pmod Ppow