(* *)
(**************************************************************************)
-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.
-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
- ]
- |assumption
- ]
-qed.
-
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))).
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 *)