@(div_mod_spec_to_eq (a*b) b … O (div_mod_spec_div_mod …))
// @div_mod_spec_intro // qed.
-(*
theorem div_n_n: ∀n:nat. O < n → n / n = 1.
/2/ qed.
theorem mod_n_n: ∀n:nat. O < n → n \mod n = O.
#n #posn
@(div_mod_spec_to_eq2 n n … 1 0 (div_mod_spec_div_mod …))
-/2/ qed. *)
+/2/ qed.
theorem mod_S: ∀n,m:nat. O < m → S (n \mod m) < m →
((S n) \mod m) = S (n \mod m).
#n #m #posm #H
@(div_mod_spec_to_eq2 (S n) m … (n / m) ? (div_mod_spec_div_mod …))
-// @div_mod_spec_intro// (applyS eq_f) //
+// @div_mod_spec_intro// applyS eq_f //
qed.
theorem mod_O_n: ∀n:nat.O \mod n = O.
((S (n \mod q)<q) ∧ S n = (div n q) * q + S (n\mod q))).
#n #q #posq
(elim (le_to_or_lt_eq ?? (lt_mod_m_m n q posq))) #H
- [%2 % // (applyS eq_f) //
+ [%2 % // applyS eq_f //
|%1 % // /demod/ <H in ⊢(? ? ? (? % ?)) @eq_f//
]
qed.
]
qed. *)
-theorem le_plus_to_minus_r: ∀a,b,c. a + b ≤ c → a ≤ c -b.
-#a #b #c #H @(le_plus_to_le_r … b) /2/
-qed.
-
-theorem le_minus_to_plus_r: ∀a,b,c. c ≤ b → a ≤ b - c → a + c ≤ b.
-#a #b #c #Hlecb #H >(plus_minus_m_m … Hlecb) /2/
-qed.
-
-theorem lt_minus_to_plus: ∀a,b,c. a - b < c → a < c + b.
-#a #b #c #H @not_le_to_lt
-@(not_to_not … (lt_to_not_le …H)) /2/
-qed.
-
-theorem lt_minus_to_plus_r: ∀a,b,c. c ≤ a →
- a < b + c → a - c < b.
-#a #b #c #lea #H @not_le_to_lt
-@(not_to_not … (lt_to_not_le …H)) /2/
-qed.
-
theorem lt_to_le_times_to_lt_S_to_div: ∀a,c,b:nat.
O < b → (b*c) ≤ a → a < (b*(S c)) → a/b = c.
#a #c #b #posb#lea #lta
@(div_mod_spec_to_eq … (a-b*c) (div_mod_spec_div_mod … posb …))
-@div_mod_spec_intro [@lt_minus_to_plus_r // |/2/]
+@div_mod_spec_intro [@lt_plus_to_minus // |/2/]
qed.
theorem div_times_times: ∀a,b,c:nat. O < c → O < b →
@(div_mod_spec_to_eq2 (a*c) (b*c) (a/b) ((a*c) \mod (b*c)) (a/b) (c*(a \mod b)))
[>(div_times_times … posc) // @div_mod_spec_div_mod /2/
|@div_mod_spec_intro
- [(applyS monotonic_lt_times_l) /2/
+ [applyS (monotonic_lt_times_r … c posc) /2/
|(applyS (eq_f …(λx.x*c))) //
]
]