proposition: Lemma Ndiv_plus_simpl : forall a b c, (a | b + c) -> (a | b) -> (a | c).
proof: Proof. intros. destruct b. destruct H. apply Ndivide_intro with q. auto with arith. destruct H. destruct H0. apply Ndivide_intro with (q-q0). assert (q0<=q). apply Nquotient_le_compat with a (S b) (S b+c). apply Nquotient_intro. exact H0. apply Nquotient_intro. exact H. split. auto with arith. auto with arith. apply Nle_plus in H1. destruct H1. rewrite H1. assert (q0+x-q0=x). rewrite <- Nat.add_comm. apply Nat.add_sub. rewrite H2. rewrite H1 in H. rewrite H0 in H. rewrite Nat.mul_add_distr_r in H. rewrite Nat.add_comm in H. apply Nat.add_cancel_l with (q0*a). rewrite Nat.add_comm. rewrite H. auto with arith. Qed.
imports: Coq(Arith Euclid Compare Lia)