From 5cad8d0d44e4e776d0ba311ef8676b5a09a60759 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Mon, 5 Aug 2024 11:13:19 +0100 Subject: [PATCH] Nat: distributivity of multiplication over subtraction Signed-off-by: Ali Caglayan --- theories/Spaces/Nat/Core.v | 27 +++++++++++++++++++++++++++ 1 file changed, 27 insertions(+) diff --git a/theories/Spaces/Nat/Core.v b/theories/Spaces/Nat/Core.v index d96d70f12ce..c43c89378f3 100644 --- a/theories/Spaces/Nat/Core.v +++ b/theories/Spaces/Nat/Core.v @@ -1174,6 +1174,33 @@ Proof. exact IHleq. Defined. +(** Multiplication on the left distributes over subtraction. *) +Definition nat_dist_sub_l n m k + : n * (m - k) = n * m - n * k. +Proof. + induction n as [|n IHn] in m, k |- *. + 1: reflexivity. + destruct (leq_dichotomy k m) as [l|r]. + - simpl; rewrite IHn, <- nat_sub_l_add_r, <- nat_sub_l_add_l, + nat_sub_r_add; trivial; exact _. + - apply leq_lt in r. + apply equiv_nat_sub_leq in r. + rewrite r. + rewrite nat_mul_zero_r. + symmetry. + apply equiv_nat_sub_leq. + apply nat_mul_l_monotone. + by apply equiv_nat_sub_leq. +Defined. + +(** Multiplication on the right distributes over subtraction. *) +Definition nat_dist_sub_r n m k + : (n - m) * k = n * k - m * k. +Proof. + rewrite 3 (nat_mul_comm _ k). + apply nat_dist_sub_l. +Defined. + (** *** Monotonicity of subtraction *) (** Subtraction is monotone in the left argument. *)