Remove add_mul_diff

Too specific and one liner with existing MathComp lemmas.

analysis/facts/hyperperiod.v

@@ -133,8 +133,8 @@ Section PeriodicLemmas.
       size (jobs_in_hyperperiod ts arr_seq (n2 * HP + O_max) tsk).
   Proof.
     intros * N1_LT.
-    specialize (add_mul_diff n1 n2 HP O_max) => AD; feed_n 1 AD => //.
-    rewrite AD.
+    have -> : n2 * HP + O_max = n1 * HP + O_max + (n2 - n1) * HP.
+    { by rewrite -[in LHS](subnKC N1_LT) mulnDl addnAC. }
     destruct (hyperperiod_int_mult_of_any_task ts tsk H_task_in_ts) as [k HYP]; rewrite !/HP.
     rewrite [in X in _ = size (_ (n1 * HP + O_max + _ * X) tsk)]HYP.
     rewrite mulnA /HP /jobs_in_hyperperiod !size_of_task_arrivals_between.

util/nat.v

@@ -23,20 +23,6 @@ Section NatLemmas.
     by move=> /(leq_trans (ltn_addr _ pltm)); rewrite ltnn.
   Qed.
 
-  (** The expression [n2 * a + b] can be written as [n1 * a + b + (n2 - n1) * a]
-      for any integer [n1] such that [n1 <= n2]. *)
-  Lemma add_mul_diff:
-    forall n1 n2 a b,
-      n1 <= n2 ->
-      n2 * a + b = n1 * a + b + (n2 - n1) * a.
-  Proof.
-    intros * LT.
-    rewrite mulnBl.
-    rewrite addnBA; first by lia.
-    destruct a; first by lia.
-    by rewrite leq_pmul2r.
-  Qed.
-
   (** Given constants [a, b, c, z] such that [b <= a], if there is no
       constant [m] such that [a = b + m * c], then it holds that there
       is no constant [n] such that [a + z * c = b + n * c]. *)