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