(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/nat/div_and_mod".
-
include "datatypes/constructors.ma".
include "nat/minus.ma".
-
let rec mod_aux p m n: nat \def
match (leb m n) with
[ true \Rightarrow m
|apply div_mod_spec_intro[assumption|reflexivity]
]
qed.
+
(* some properties of div and mod *)
theorem div_times: \forall n,m:nat. ((S n)*m) / (S n) = m.
intros.
]
qed.
-theorem le_div: \forall n,m. O < n \to m/n \le m.
+theorem or_div_mod: \forall n,q. O < q \to
+((S (n \mod q)=q) \land S n = (S (div n q)) * q \lor
+((S (n \mod q)<q) \land S n= (div n q) * q + S (n\mod q))).
intros.
-rewrite > (div_mod m n) in \vdash (? ? %)
- [apply (trans_le ? (m/n*n))
- [rewrite > times_n_SO in \vdash (? % ?).
- apply le_times
- [apply le_n|assumption]
- |apply le_plus_n_r
+elim (le_to_or_lt_eq ? ? (lt_mod_m_m n q H))
+ [right.split
+ [assumption
+ |rewrite < plus_n_Sm.
+ apply eq_f.
+ apply div_mod.
+ assumption
+ ]
+ |left.split
+ [assumption
+ |simplify.
+ rewrite > sym_plus.
+ rewrite < H1 in ⊢ (? ? ? (? ? %)).
+ rewrite < plus_n_Sm.
+ apply eq_f.
+ apply div_mod.
+ assumption
]
- |assumption
]
qed.
variant inj_times_l1:\forall n. O < n \to \forall p,q:nat.p*n = q*n \to p=q
\def lt_O_to_injective_times_l.
+
(* n_divides computes the pair (div,mod) *)
(* p is just an upper bound, acc is an accumulator *)