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
injective_times_r.
theorem lt_O_to_injective_times_r: \forall n:nat. O < n \to injective nat nat (\lambda m:nat.n*m).
-change with (\forall n. O < n \to \forall p,q:nat.n*p = n*q \to p=q).
+simplify.
intros 4.
apply (lt_O_n_elim n H).intros.
apply (inj_times_r m).assumption.
\def lt_O_to_injective_times_r.
theorem injective_times_l: \forall n:nat.injective nat nat (\lambda m:nat.m*(S n)).
-change with (\forall n,p,q:nat.p*(S n) = q*(S n) \to p=q).
+simplify.
intros.
-apply (inj_times_r n p q).
+apply (inj_times_r n x y).
rewrite < sym_times.
-rewrite < (sym_times q).
+rewrite < (sym_times y).
assumption.
qed.
injective_times_l.
theorem lt_O_to_injective_times_l: \forall n:nat. O < n \to injective nat nat (\lambda m:nat.m*n).
-change with (\forall n. O < n \to \forall p,q:nat.p*n = q*n \to p=q).
+simplify.
intros 4.
apply (lt_O_n_elim n H).intros.
apply (inj_times_l m).assumption.
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 *)
+let rec n_divides_aux p n m acc \def
+ match n \mod m with
+ [ O \Rightarrow
+ match p with
+ [ O \Rightarrow pair nat nat acc n
+ | (S p) \Rightarrow n_divides_aux p (n / m) m (S acc)]
+ | (S a) \Rightarrow pair nat nat acc n].
+
+(* n_divides n m = <q,r> if m divides n q times, with remainder r *)
+definition n_divides \def \lambda n,m:nat.n_divides_aux n n m O.