proposition: Lemma Ndiv_minus_simpl_l : forall a b c, b >= c -> (a | b - c) -> (a | b) -> (a | c).
proof: Proof. intros. apply Nle_plus in H. destruct H. rewrite H in * |- *. rewrite Nat.add_comm in H0. rewrite Nat.add_sub in H0. rewrite Nat.add_comm in H1. apply Ndiv_plus_simpl with x; auto. Qed.
imports: Coq(Arith Euclid Compare Lia)