proposition: Lemma Ndiv_plus_compat : forall p a b, (p | a) -> (p | b) -> (p | a + b).
proof: Proof. intros. destruct H. destruct H0. apply Ndivide_intro with (q+q0). rewrite H. rewrite H0. ring. Qed.
imports: Coq(Arith Euclid Compare Lia)