proposition: Remark minus_eq_decompose : forall a b c d : nat, a = b -> c = d -> a - c = b - d.
proof: Proof. intros a b c d H H0; rewrite H; rewrite H0; auto. Qed.
imports: Coq(ArithRing) Coq(Compare_dec) Coq(Wf_nat) Coq(Arith) Coq(Lia)