Require Import Bool.
Require Import Arith.
Require Import ZArith.
Require Import String.
Require Import Vbase.

Set Implicit Arguments.
Unset Strict Implicit.

Fixpoint eqn_rec (x y: nat) {struct x} :=
   match x, y with
     | O, O ⇒ true
     | S x, S y ⇒ eqn_rec x y
     | _, _ ⇒ false
   end.

Definition eqn := match tt with tt ⇒ eqn_rec end.

Lemma eqnP: ∀ x y, reflect (x = y) (eqn x y).
Proof.
  induction[] x [y]; vauto.
  change (eqn (S x) (S y)) with (eqn x y).
  case IHx; constructor; congruence.
Qed.

Canonical Structure nat_eqMixin := EqMixin eqnP.
Canonical Structure nat_eqType := Eval hnf in EqType nat nat_eqMixin.

Lemma eqnE : eqn = (@eq_op _).
Proof. done. Qed.

Inductive bool3 := B3tt | B3ff | B3un.

Definition bool3_beq (x y : bool3) :=
  match x, y with
    | B3tt, B3tt ⇒ true
    | B3ff, B3ff ⇒ true
    | B3un, B3un ⇒ true
    | _, _ ⇒ false
  end.

Lemma bool3P : ∀ x y, reflect (x = y) (bool3_beq x y).
Proof. intros[][]; vauto. Qed.

Definition negb3 (b:bool3) : bool3 :=
  match b with
   | B3tt ⇒ B3ff
   | B3ff ⇒ B3tt
   | B3un ⇒ B3un
  end.

Definition andb3 (b1 b2:bool3) : bool3 :=
  match b1, b2 with
    | B3tt, _ ⇒ b2
    | B3ff, _ ⇒ B3ff
    | B3un, B3ff ⇒ B3ff
    | B3un, _ ⇒ B3un
  end.

Definition orb3 (b1 b2:bool3) : bool3 :=
  match b1, b2 with
    | B3tt, _ ⇒ B3tt
    | B3ff, _ ⇒ b2
    | B3un, B3tt ⇒ B3tt
    | B3un, _ ⇒ B3un
  end.

Definition bool2bool3 (b: bool) : bool3 :=
  if b then B3tt else B3ff.

Definition b3_moredef (b1 : bool3) (b2: bool) : bool :=
  match b1 with
    | B3tt ⇒ b2
    | B3ff ⇒ negb b2
    | B3un ⇒ false
  end.

Lemma andb3T: ∀ b, andb3 b B3tt = b.
Proof. by intros[]. Qed.
Lemma andb3F: ∀ b, andb3 b B3ff = B3ff.
Proof. by intros[]. Qed.
Lemma orb3T: ∀ b, orb3 b B3tt = B3tt.
Proof. by intros[]. Qed.
Lemma orb3F: ∀ b, orb3 b B3ff = b.
Proof. by intros[]. Qed.

Lemma negb3P: ∀ x, bool2bool3 (negb x) = negb3 (bool2bool3 x).
Proof. by destruct x. Qed.

Lemma andb3P: ∀ x y, bool2bool3 (andb x y) = andb3 (bool2bool3 x) (bool2bool3 y).
Proof. by intros [] []. Qed.

Lemma orb3P: ∀ x y, bool2bool3 (orb x y) = orb3 (bool2bool3 x) (bool2bool3 y).
Proof. by intros [] []. Qed.

Lemma negb3_neg : ∀ x, negb3 (negb3 x) = x.
Proof. by intros []. Qed.

Lemma negb3_and : ∀ b1 b2, negb3 (andb3 b1 b2) = orb3 (negb3 b1) (negb3 b2).
Proof. by intros [] []. Qed.

Lemma negb3_or : ∀ b1 b2, negb3 (orb3 b1 b2) = andb3 (negb3 b1) (negb3 b2).
Proof. by intros [] []. Qed.

Hint Rewrite negb3_neg negb3_and negb3_or negb3P andb3P orb3P : vlib.

Delimit Scope coq_nat_scope with coq_nat.

Notation "m <= n" := (le m n) : coq_nat_scope.
Notation "m < n" := (lt m n) : coq_nat_scope.
Notation "m >= n" := (ge m n) : coq_nat_scope.
Notation "m > n" := (gt m n) : coq_nat_scope.

Inductive LtSpec (A : Type) (le lt : A → A → Prop) (x y: A): bool → Prop :=
  | LtSpecLt : lt x y → LtSpec le lt x y true
  | LtSpecGe : le y x → LtSpec le lt x y false.

Inductive CmpSpecFull (A : Type) (lt : A → A → Prop) (x y: A)
  : bool → bool → bool → bool → bool → bool → comparison → Prop :=
  | CmpSpecLt : lt x y → CmpSpecFull lt x y true true false false false false Lt
  | CmpSpecEq : x = y → CmpSpecFull lt x y false true true true false true Eq
  | CmpSpecGt : lt y x → CmpSpecFull lt x y false false false false true true Gt.

Definition len (m n:nat) := match tt with tt ⇒ leb m n end.

Definition ltn m n := len (S m) n.

Notation "m <= n" := (len m n) : nat_scope.
Notation "m < n" := (ltn m n) : nat_scope.
Notation "m >= n" := (n ≤ m) (only parsing) : nat_scope.
Notation "m > n" := (n < m) (only parsing) : nat_scope.

Lemma add0n : ∀ n, 0 + n = n.
Proof. done. Qed.
Lemma addSn : ∀ m n, S m + n = S (m + n).
Proof. done. Qed.
Lemma add1n : ∀ n, 1 + n = S n.
Proof. done. Qed.
Lemma addn0 : ∀ x, x + 0 = x.
Proof. auto with arith. Qed.
Lemma addnS : ∀ m n, m + (S n) = S (m + n).
Proof. auto with arith. Qed.
Lemma addn1 : ∀ n, n + 1 = S n.
Proof. intros; omega. Qed.
Lemma addSnnS : ∀ m n, S m + n = m + (S n).
Proof. intros; omega. Qed.

Lemma addnC : ∀ x y, x + y = y + x.
Proof. intros; omega. Qed.
Lemma addnA : ∀ x y z, x + (y + z) = x + y + z.
Proof. intros; omega. Qed.
Lemma addnCA : ∀ x y z, x + (y + z) = y + (x + z).
Proof. intros; omega. Qed.
Lemma addnAC : ∀ x y z, x + y + z = x + z + y.
Proof. intros; omega. Qed.

Lemma addn_eq0 : ∀ m n, (m + n == 0) = (m == 0) && (n == 0).
Proof. by intros; induction m. Qed.

Lemma eqn_addl : ∀ p m n, (p + m == p + n) = (m == n).
Proof. by intros; induction p. Qed.

Lemma eqn_addr : ∀ p m n, (m + p == n + p) = (m == n).
Proof. by intros; rewrite (addnC m), (addnC n), eqn_addl. Qed.

Lemma sub0n : ∀ x, 0 - x = 0.
Proof. intros; omega. Qed.
Lemma subn0 : ∀ x, x - 0 = x.
Proof. intros; omega. Qed.
Lemma subnn : ∀ x, x - x = 0.
Proof. intros; omega. Qed.
Lemma subSS : ∀ n m, S m - S n = m - n.
Proof. intros; omega. Qed.

Lemma subn_add2l : ∀ p m n, (p + m) - (p + n) = m - n.
Proof. intros; omega. Qed.
Lemma subn_add2r : ∀ p m n, (m + p) - (n + p) = m - n.
Proof. intros; omega. Qed.

Lemma subSnn : ∀ n, S n - n = 1.
Proof. intros; omega. Qed.
Lemma subn_sub : ∀ m n p, (n - m) - p = n - (m + p).
Proof. intros; omega. Qed.
Lemma subnAC : ∀ x y z, x - y - z = x - z - y.
Proof. intros; omega. Qed.

Hint Rewrite
  add0n addSn addn0 addnS addn_eq0 eqn_addl eqn_addr
  sub0n subn0 subnn subSS subn_add2l subn_add2r : vlib.

Lemma eq0S : ∀ n, (O == S n) = false.
Proof. done. Qed.
Lemma eqS0 : ∀ n, (S n == O) = false.
Proof. done. Qed.
Lemma eqSS : ∀ m n, (S m == S n) = (m == n).
Proof. done. Qed.
Lemma eqnn : ∀ n : nat, (n == n).
Proof. induction n; simpls. Qed.
Lemma eqnC : ∀ x y : nat, (x == y) = (y == x).
Proof. induct x [y]; apply IHx. Qed.

Hint Resolve eqnn.
Hint Rewrite eqnn eqSS eq0S eqS0 : vlib.

Lemma ltnE : ∀ m n, (m < n) = negb (n ≤ m).
Proof. induction m; destruct n; simpls; apply IHm. Qed.

Lemma lenE : ∀ m n, (m ≤ n) = negb (n < m).
Proof. induction m; destruct n; simpls; apply IHm. Qed.

Lemma lenE_sub : ∀ m n, (m ≤ n) = (m - n == 0).
Proof. induction m; destruct n; simpls; apply IHm. Qed.

Lemma ltnE_sub : ∀ m n, (m < n) = (m + 1 - n == 0).
Proof. induction m; destruct n; simpls; apply IHm. Qed.

Lemma leP : ∀ x y, LtSpec lt le x y (x ≤ y).
Proof.
  unfold len; intros x y; case (le_lt_dec x y); intro X;
  [rewrite leb_correct | rewrite leb_correct_conv]; vauto.
Qed.

Lemma ltP : ∀ x y, LtSpec le lt x y (x < y).
Proof. intros; rewrite ltnE; case leP; vauto. Qed.

Lemma ltn_correct: ∀ x y, (x < y)%coq_nat → x < y.
Proof. by intros; case ltP; [|intro X; apply le_not_lt in X]. Qed.

Lemma len_correct: ∀ x y, (x ≤ y)%coq_nat → x ≤ y.
Proof. by intros; case leP; [|intro X; apply lt_not_le in X]. Qed.

Lemma ltn_complete: ∀ x y, x < y → (x < y)%coq_nat.
Proof. by intros ? ?; case ltP. Qed.

Lemma len_complete: ∀ x y, x ≤ y → (x ≤ y)%coq_nat.
Proof. by intros ? ?; case leP. Qed.

Lemma lenP : ∀ x y, LtSpec ltn len x y (x ≤ y).
Proof. by intros; case_eq (x ≤ y) as H; vauto; right; rewrite ltnE, H. Qed.

Lemma ltnP : ∀ x y, LtSpec len ltn x y (x < y).
Proof. intros; rewrite ltnE; case lenP; vauto. Qed.

Lemma le0n : ∀ n, 0 ≤ n.
Proof. done. Qed.
Lemma len0 : ∀ n, (n ≤ 0) = (n == 0).
Proof. induction n; simpls. Qed.
Lemma lenn : ∀ n, n ≤ n.
Proof. induction n; simpls. Qed.
Lemma lenSn : ∀ n, n ≤ S n.
Proof. induction n; simpls. Qed.

Lemma lt0Sn : ∀ n, 0 < S n.
Proof. done. Qed.
Lemma ltn0 : ∀ n, (n < 0) = false.
Proof. intros []; simpls. Qed.
Lemma ltnn : ∀ n, (n < n) = false.
Proof. induction n; simpls. Qed.
Lemma ltnSn : ∀ n, (n < S n).
Proof. induction n; simpls. Qed.

Lemma leSS : ∀ m n, (S m ≤ S n) = (m ≤ n).
Proof. done. Qed.
Lemma ltSS : ∀ m n, (S m < S n) = (m < n).
Proof. done. Qed.

Hint Resolve lenn lenSn ltnn ltnSn.

Lemma eq_len : ∀ m n, m = n → m ≤ n.
Proof. by intros; subst. Qed.

Lemma ltnS : ∀ m n, (m < S n) = (m ≤ n).
Proof. induction m; destruct n; simpls. Qed.

Lemma leSn : ∀ m n, (S m ≤ n) = (m < n).
Proof. induction m; destruct n; simpls. Qed.

Hint Rewrite leSS le0n len0 lenn lenSn ltSS lt0Sn ltn0 ltnn ltnSn ltnS leSn : vlib.

Lemma lt0n : ∀ n, (0 < n) = negb (n == 0).
Proof. induction n; simpls. Qed.
Lemma lt0n_neq0 : ∀ n, 0 < n → negb (n == 0).
Proof. by intro; rewrite lt0n. Qed.
Lemma eqn0_Nlt0n : ∀ n, n == 0 = negb (0 < n).
Proof. by intros[]. Qed.
Lemma neq0_lt0n : ∀ n, n == 0 = false → 0 < n.
Proof. by intros; rewrite lt0n, H. Qed.
Hint Resolve lt0n_neq0 neq0_lt0n.

Lemma len_anti : ∀ m n, m ≤ n → n ≤ m → n = m.
Proof. induction m; destruct n; ins; auto. Qed.
Hint Immediate len_anti : lib.

Lemma eqn_leAle : ∀ m n, (m == n) = (m ≤ n) && (n ≤ m).
Proof. induct m [n]. Qed.

Lemma neqn_ltVlt : ∀ m n, negb (m == n) = (m < n) || (n < m).
Proof. induct m [n]. Qed.

Lemma len_eqVlt : ∀ m n, len m n = (m == n) || (m < n).
Proof. induct m [n]. Qed.

Lemma ltn_neqAle : ∀ m n, (m < n) = negb (m == n) && (m ≤ n).
Proof. induct m [n]. Qed.

Lemma len_trans : ∀ n m p, m ≤ n → n ≤ p → m ≤ p.
Proof. induct n [m p]. Qed.

Lemma len_ltn_trans : ∀ n m p, m ≤ n → n < p → m < p.
Proof. induct n [m p]. Qed.

Lemma ltn_len_trans : ∀ n m p, m < n → n ≤ p → m < p.
Proof. induct n [m p]. Qed.

Lemma ltn_trans : ∀ n m p, m < n → n < p → m < p.
Proof. induct n [m p]. Qed.

Lemma ltnW : ∀ m n, m < n → m ≤ n.
Proof. induct m [n]. Qed.
Hint Resolve ltnW.

Lemma lenW : ∀ m n, m ≤ n → m ≤ (S n).
Proof. induct m [n]. Qed.

Lemma len_total : ∀ m n, (m ≤ n) || (n ≤ m).
Proof. induct m [n]. Qed.

Lemma nat_comparenn: ∀ x, nat_compare x x = Eq.
Proof. by induction x; [|rewrite nat_compare_S]. Qed.

Lemma cmpP : ∀ x y,
  CmpSpecFull ltn x y (x < y) (x ≤ y) (x == y) (y == x) (y < x) (y ≤ x) (nat_compare x y).
Proof.
  intros; rewrite (ltnE y x), eqnC, len_eqVlt, lenE.
  case_eq (nat_compare x y); intro N.
  - by apply nat_compare_eq in N; subst; rewrite ltnn, eqnn; vauto.
  - apply nat_compare_lt, ltn_correct in N.
    rewrite N, orbT; simpl.
    by case eqnP; vauto; intros; clarify; autorewrite with vlib in N.
  - apply nat_compare_gt, ltn_correct in N.
    rewrite <-len_eqVlt, <- lenE; rewrite ltnE, len_eqVlt, lenE.
    rewrite N, orbT; simpl.
    by case eqnP; vauto; intros; clarify; autorewrite with vlib in N.
Qed.

Lemma len_add2l : ∀ p m n, (p + m ≤ p + n) = (m ≤ n).
Proof. induction p; simpls. Qed.

Lemma ltn_add2l : ∀ p m n, (p + m < p + n) = (m < n).
Proof. induction p; simpls. Qed.

Lemma len_add2r : ∀ p m n, (m + p ≤ n + p) = (m ≤ n).
Proof. intros; rewrite (addnC n), (addnC m); apply len_add2l. Qed.

Lemma ltn_add2r : ∀ p m n, (m + p < n + p) = (m < n).
Proof. intros; rewrite (addnC n), (addnC m); apply ltn_add2l. Qed.

Lemma len_add : ∀ m1 m2 n1 n2,
  m1 ≤ n1 → m2 ≤ n2 → m1 + m2 ≤ n1 + n2.
Proof. intros????; repeat (case leP; simpls); intros; elimtype False; omega. Qed.

Lemma len_addr : ∀ m n, n ≤ n + m.
Proof. induction n; simpls. Qed.

Lemma len_addl : ∀ m n, n ≤ m + n.
Proof. by intros; rewrite addnC; apply len_addr. Qed.

Lemma ltn_addr : ∀ m n p, m < n → m < n + p.
Proof. induction m; destruct n; intros; clarify; autorewrite with vlib; auto. Qed.

Lemma ltn_addl : ∀ m n p, m < n → m < p + n.
Proof. by intros; rewrite addnC; apply ltn_addr. Qed.

Lemma lt0_addn : ∀ m n, (0 < m + n) = (0 < m) || (0 < n).
Proof. by intros [] []. Qed.

Lemma lt0_subn : ∀ m n, (0 < n - m) = (m < n).
Proof. induction m; destruct n; autorewrite with vlib; simpls. Qed.

Lemma subn_eq0 : ∀ m n, (m - n == 0) = (m ≤ n).
Proof. induction m; destruct n; autorewrite with vlib; simpls. Qed.

Lemma len_sub_add : ∀ m n p, (m - n ≤ p) = (m ≤ n + p).
Proof. induction m; destruct n; intros; autorewrite with vlib; simpls. Qed.

Lemma len_subr : ∀ m n, n - m ≤ n.
Proof. eby induction m; destruct n; simpls; eapply len_trans. Qed.

Lemma subnKC : ∀ m n, m ≤ n → m + (n - m) = n.
Proof. induction m; destruct n; simpls; auto. Qed.

Lemma subnK : ∀ m n, m ≤ n → (n - m) + m = n.
Proof. by intros; rewrite addnC; apply subnKC. Qed.

Lemma addn_subA : ∀ m n p, p ≤ n → m + (n - p) = m + n - p.
Proof. intros???; case leP; ins; omega. Qed.

Lemma subn_subA : ∀ m n p, p ≤ n → m - (n - p) = m + p - n.
Proof. intros???; case leP; ins; omega. Qed.

Lemma subKn : ∀ m n, m ≤ n → n - (n - m) = m.
Proof. intros??; case leP; ins; omega. Qed.

Lemma len_subS : ∀ m n, m ≤ n → S n - m = S (n - m).
Proof. induct m [n]. Qed.

Lemma ltn_subS : ∀ m n, m < n → n - m = S (n - S m).
Proof. induct m [n]. Qed.

Lemma len_sub2r : ∀ p m n, (m ≤ n) → (m - p ≤ n - p).
Proof. intros ???; case leP; case leP; ins; omega. Qed.

Lemma len_sub2l : ∀ p m n, m ≤ n → p - n ≤ p - m.
Proof. intros ???; case leP; case leP; ins; omega. Qed.

Lemma len_sub2 : ∀ m1 m2 n1 n2,
  m1 ≤ m2 → n2 ≤ n1 → m1 - n1 ≤ m2 - n2.
Proof. intros????; repeat (case leP; simpls); ins; omega. Qed.

Lemma ltn_sub2r : ∀ p m n, p < n → m < n → m - p < n - p.
Proof. intros???; repeat (case ltP; simpls); ins; omega. Qed.

Lemma ltn_sub2l : ∀ p m n, m < p → m < n → p - n < p - m.
Proof. intros???; repeat (case ltP; simpls); ins; omega. Qed.

Lemma ltn_add_sub : ∀ m n p, (m + n < p) = (n < p - m).
Proof. intros???; repeat (case ltP; simpls); ins; omega. Qed.

Lemma lenE_diff: ∀ m n, m ≤ n → ∃ k, n = m + k.
Proof.
  induction m; destruct n; ins; [by ∃ 0|by ∃ (S n)|].
  by destruct (IHm _ H) as [x ?]; ∃ x; f_equal.
Qed.

Lemma ltnE_diff: ∀ m n, m < n → ∃ k, n = S (m + k).
Proof.
  induction m; destruct n; ins; [by ∃ n|].
  by destruct (IHm _ H) as [x ?]; ∃ x; f_equal.
Qed.

Lemma len_subnE : ∀ m n, (m ≤ m - n) = (n == 0) || (m == 0).
Proof.
  by intros[][]; intros; clarify; autorewrite with vlib; clarify;
    rewrite <- ltn_add_sub, ltnE, len_addl.
Qed.

Lemma mul0n : ∀ n, 0 × n = 0.
Proof. done. Qed.
Lemma muln0 : ∀ n, n × 0 = 0.
Proof. induction n; simpls. Qed.
Lemma mul1n : ∀ n, 1 × n = n.
Proof. intros; simpl; apply addn0. Qed.
Lemma muln1 : ∀ n, n × 1 = n.
Proof. induction n; simpls; auto. Qed.

Lemma mulSn : ∀ m n, S m × n = n + m × n.
Proof. done. Qed.
Lemma mulSnr : ∀ m n, S m × n = m × n + n.
Proof. intros; simpl; apply addnC. Qed.
Lemma mulnS : ∀ m n, m × S n = m + m × n.
Proof. by induction m; ins; rewrite IHm, addnCA. Qed.
Lemma mulnSr : ∀ m n, m × S n = m × n + m.
Proof. intros; rewrite mulnS; apply addnC. Qed.

Lemma mulnC : ∀ m n, m × n = n × m.
Proof. by induction n; simpls; rewrite mulnS, IHn. Qed.

Lemma muln_addl : ∀ x y z, (x + y) × z = x × z + y × z.
Proof. by intros; induction x; simpls; rewrite IHx, addnA. Qed.

Lemma muln_addr : ∀ x y z, x × (y + z) = x × y + x × z.
Proof. intros; rewrite mulnC, muln_addl; f_equal; apply mulnC. Qed.

Lemma muln_subl : ∀ x y z, (x - y) × z = x × z - y × z.
Proof. auto with arith. Qed.

Lemma muln_subr : ∀ x y z, x × (y - z) = x × y - x × z.
Proof. auto with arith. Qed.

Lemma mulnA : ∀ x y z, x × (y × z) = x × y × z.
Proof. auto with arith. Qed.

Lemma mulnCA : ∀ x y z, x × (y × z) = y × (x × z).
Proof. by intros; rewrite mulnA, (mulnC x), mulnA. Qed.

Lemma mulnAC : ∀ x y z, x × y × z = x × z × y.
Proof. by intros; rewrite <- mulnA, (mulnC y), mulnA. Qed.

Lemma eqn_mul0 : ∀ m n, (m × n == 0) = (m == 0) || (n == 0).
Proof. by intros[][]; simpls; rewrite muln0. Qed.

Lemma eqn_mul1 : ∀ m n, (m × n == 1) = (m == 1) && (n == 1).
Proof. by intros[|[]][|[]]; simpls; rewrite ?muln0. Qed.

Lemma lt0_muln : ∀ m n, (0 < m × n) = (0 < m) && (0 < n).
Proof. by intros[][]; simpls; rewrite muln0. Qed.

Lemma len_pmull : ∀ m n, 0 < n → m ≤ n × m.
Proof. destruct n; ins; apply len_addr. Qed.

Lemma len_pmulr : ∀ m n, 0 < n → m ≤ m × n.
Proof. intros[][]; ins; rewrite mulnS, addnCA; apply len_addr. Qed.

Lemma len_mul2l : ∀ m n1 n2, (m × n1 ≤ m × n2) = (m == 0) || (n1 ≤ n2).
Proof.
intros; rewrite !lenE_sub, <- muln_subr; destruct m; simpls.
by destruct (n1 - n2); simpls; rewrite muln0.
Qed.

Lemma len_mul2r : ∀ m n1 n2, (n1 × m ≤ n2 × m) = (m == 0) || (n1 ≤ n2).
Proof. by intros; rewrite <- len_mul2l, !(mulnC m). Qed.

Lemma len_mul : ∀ m1 m2 n1 n2, m1 ≤ n1 → m2 ≤ n2 → m1 × m2 ≤ n1 × n2.
Proof.
intros; destruct (lenE_diff H); destruct (lenE_diff H0); subst.
rewrite muln_addl; eapply len_trans, len_addr.
by rewrite muln_addr; eapply len_trans, len_addr.
Qed.

Lemma eqn_mul2l : ∀ m n1 n2, (m × n1 == m × n2) = (m == 0) || (n1 == n2).
Proof.
destruct m; simpls; intros; rewrite !(mulnC m).
revert n2; induction n1; destruct n2; autorewrite with vlib; simpls.
by rewrite <- IHn1, !(addnC m), !addnA, eqn_addr.
Qed.

Lemma eqn_mul2r : ∀ m n1 n2, (n1 × m == n2 × m) = (m == 0) || (n1 == n2).
Proof. by intros; rewrite <- !(mulnC m), eqn_mul2l. Qed.

Lemma len_pmul2l : ∀ m n1 n2, 0 < m → (m × n1 ≤ m × n2) = (n1 ≤ n2).
Proof. by intros; rewrite len_mul2l; destruct m. Qed.
Implicit Arguments len_pmul2l [m n1 n2].

Lemma len_pmul2r : ∀ m n1 n2, 0 < m → (n1 × m ≤ n2 × m) = (n1 ≤ n2).
Proof. by intros; rewrite len_mul2r; destruct m. Qed.
Implicit Arguments len_pmul2r [m n1 n2].

Lemma eqn_pmul2l : ∀ m n1 n2, 0 < m → (m × n1 == m × n2) = (n1 == n2).
Proof. by intros; rewrite eqn_mul2l; destruct m. Qed.
Implicit Arguments eqn_pmul2l [m n1 n2].

Lemma eqn_pmul2r : ∀ m n1 n2, 0 < m → (n1 × m == n2 × m) = (n1 == n2).
Proof. by intros; rewrite eqn_mul2r; destruct m. Qed.
Implicit Arguments eqn_pmul2r [m n1 n2].

Lemma ltn_mul2l : ∀ m n1 n2, (m × n1 < m × n2) = (0 < m) && (n1 < n2).
Proof.
destruct m; simpls; intros; rewrite !(mulnC m).
revert n2; induction n1; destruct n2; autorewrite with vlib; simpls.
by rewrite <- IHn1, !(addnC m), !addnA; rewrite ltn_add2r.
Qed.

Lemma ltn_mul2r : ∀ m n1 n2, (n1 × m < n2 × m) = (0 < m) && (n1 < n2).
Proof. by intros; rewrite <- !(mulnC m), ltn_mul2l. Qed.

Lemma ltn_pmul2l : ∀ m n1 n2, 0 < m → (m × n1 < m × n2) = (n1 < n2).
Proof. by intros; rewrite ltn_mul2l; destruct m. Qed.
Implicit Arguments ltn_pmul2l [m n1 n2].

Lemma ltn_pmul2r : ∀ m n1 n2, 0 < m → (n1 × m < n2 × m) = (n1 < n2).
Proof. by intros; rewrite ltn_mul2r; destruct m. Qed.
Implicit Arguments ltn_pmul2r [m n1 n2].

Lemma ltn_mul : ∀ m1 m2 n1 n2, m1 < n1 → m2 < n2 → m1 × m2 < n1 × n2.
Proof.
intros; rewrite <- leSn in *; eapply len_trans, len_mul; try eassumption.
by simpls; autorewrite with vlib; eapply len_trans, len_addl; rewrite len_mul2l, lenSn, orbT.
Qed.

Lemma ltn_Pmull : ∀ m n, 1 < n → 0 < m → m < n × m.
Proof. by intros; rewrite <- (mul1n m) at 1; rewrite ltn_mul2r, H, H0. Qed.

Lemma ltn_Pmulr : ∀ m n, 1 < n → 0 < m → m < m × n.
Proof. by intros; rewrite <- (muln1 m) at 1; rewrite ltn_mul2l, H, H0. Qed.

Lemma lenS : ∀ m n, n ≤ m → n ≤ S m.
Proof. eauto using len_trans. Qed.

Lemma ltn_of_leS : ∀ n m : nat, (n < m) → (S n ≤ m).
Proof. by intros; rewrite leSn. Qed.

Lemma leSn_of_lt : ∀ n m : nat, (S n ≤ m) → (n < m).
Proof. by intros; rewrite <- leSn. Qed.

Lemma len_mul2l_imp : ∀ m n1 n2, n1 ≤ n2 → (m × n1 ≤ m × n2).
Proof. by intros; rewrite len_mul2l, H, orbT. Qed.

Lemma len_mul2r_imp : ∀ m n1 n2, n1 ≤ n2 → (n1 × m ≤ n2 × m).
Proof. by intros; rewrite len_mul2r, H, orbT. Qed.

Hint Resolve lenS len_addl len_addr len_trans len_add2r len_add2l len_sub2r len_sub2l
             len_mul2l_imp len_mul2r_imp : vlib.
Hint Immediate ltn_of_leS leSn_of_lt: vlib.

Hint Rewrite add0n addSn addn0 addnS addn_eq0 eqn_addl eqn_addr
  sub0n subn0 subnn subSS subn_add2l subn_add2r
  nat_comparenn
  len_add2l ltn_add2l len_add2r ltn_add2r len_addr len_addl
  lt0_addn lt0_subn len_sub_add len_subnE
  mul0n muln0 mul1n muln1

  muln_addl muln_addr muln_subl muln_subr
  eqn_mul0 eqn_mul1 lt0_muln
  len_mul2l len_mul2r eqn_mul2l eqn_mul2r ltn_mul2l ltn_mul2r : vlib.

Hint Rewrite addnA mulnA : vlibA.

Fixpoint iter (A : Type) n (f : A → A) (v : A): A :=
  match n with
    | O ⇒ v
    | S n ⇒ f (iter n f v)
  end.

Fixpoint iter_rec (A : Type) n (f : A → A) (v : A): A :=
  match n with
    | O ⇒ v
    | S n ⇒ iter_rec n f (f v)
  end.

Lemma iter_recS: ∀ A n f (v: A), iter_rec (S n) f v = f (iter_rec n f v).
Proof. by induction n; intros; simpl; [|rewrite <- IHn]. Qed.

Lemma iter_recE: ∀ A n f (v: A), iter_rec n f v = iter n f v.
Proof. by induction n; intros; [|rewrite iter_recS, IHn]. Qed.

Section ZZZ.

Local Open Scope Z_scope.

Lemma Zplus_mod_same: ∀ a n : Z, (a + n) mod n = a mod n.
Proof.
  by intros; rewrite Zplus_mod, Z_mod_same_full, Zplus_0_r, Zmod_mod.
Qed.

Lemma Zmod_too_small:
  ∀ a n, -n ≤ a < 0 → a mod n = n + a.
Proof.
  intros. rewrite <- Zplus_mod_same, Zmod_small; omega.
Qed.

Lemma Zmod_too_big:
  ∀ a n, n ≤ a < n + n → a mod n = a - n.
Proof.
  intros; rewrite <- (Zminus_0_r a) at 1;
  rewrite <- (Z_mod_same_full n), Zminus_mod_idemp_r, Zmod_small; omega.
Qed.

Lemma Zopp_mod_idemp: ∀ a m, - (a mod m) mod m = - a mod m.
Proof. by apply (Zminus_mod_idemp_r 0). Qed.

Lemma Zmod_opp_expand: ∀ a b, - a mod b = (b - a) mod b.
Proof.
intros; rewrite <- (Zplus_mod_same); f_equal; omega.
Qed.

Lemma Zmod_eqD :
  ∀ a b m (H: a mod m = b mod m) (NEQ: m ≠ 0), ∃ k, a = b + k × m.
Proof.
  intros; apply Zeq_minus, (f_equal (fun x ⇒ Zmod x m)) in H.
  rewrite <- Zminus_mod, Zmod_0_l in H.
  ∃ ((a - b) / m).
  pose proof (Z.div_mod (a - b) _ NEQ); rewrite H in ×.
  rewrite Z.mul_comm; omega.
Qed.

Lemma ZdoubleE: ∀ x, Zdouble x = x × 2.
Proof. by intros; rewrite Zmult_comm. Qed.

Lemma ZltP:
  ∀ x y, LtSpec Zle Zlt x y (Zlt_bool x y).
Proof.
  intros; unfold Zlt_bool, Zle_bool.
  by case_eq (Zcompare x y); simpl; constructor; try done;
     (unfold Zle; rewrite <- (Zcompare_antisym), H).
Qed.

Lemma ZleP:
  ∀ x y, LtSpec Zlt Zle x y (Zle_bool x y).
Proof.
  intros; unfold Zlt_bool, Zle_bool.
  case_eq (Zcompare x y); simpl; constructor;
    try (by unfold Zle; rewrite H);
    try (by unfold Zlt; rewrite <- (Zcompare_antisym), H).
Qed.

Lemma ZcmpP:
  ∀ x y, CmpSpecFull Zlt x y
    (Zlt_bool x y) (Zle_bool x y) (Zeq_bool x y) (Zeq_bool y x)
    (Zlt_bool y x) (Zle_bool y x) (Zcompare x y).
Proof.
  intros; unfold Zlt_bool, Zle_bool, Zeq_bool; rewrite <- (Zcompare_antisym x).
  case_eq (Zcompare x y); simpl; constructor; try done.
    by eapply Zcompare_Eq_eq.
  by unfold Zlt; rewrite <- (Zcompare_antisym), H.
Qed.

End ZZZ.

Hint Rewrite
  Zmod_0_l Z_mod_same_full
  Zplus_mod_idemp_l Zplus_mod_idemp_r
  Zminus_mod_idemp_l Zminus_mod_idemp_r Zopp_mod_idemp : vlib.