proposition: Lemma minus_L2 : forall n p q, n>=p+q -> n-p-q=n-(p+q).
proof: Proof. intros. apply Nle_plus in H. destruct H. rewrite H. rewrite Nat.add_comm at 2. rewrite Nat.add_sub. replace (p+q+x-p) with (q+x). rewrite Nat.add_comm. rewrite Nat.add_sub. auto. rewrite <- Nat.add_assoc. rewrite (Nat.add_comm p). rewrite Nat.add_sub. auto. Qed.
imports: Coq(Arith Lia)