addons/teach/Makefile

+.PHONY: all get
+
+all:
+	# not parallel: some Dune dependency mixup with generating META file
+	dune build -j1

addons/teach/README.md

+# addon-equations
+Coq-Equations addon plugin for jsCoq

addons/teach/dune

+(rule
+ (targets coq-pkgs)
+ (deps
+  (package teach)
+  (:pkg-json teach-pkg.json))
+ (action
+  (run jscoq build %{pkg-json})))
+
+(dirs workdir)
\ No newline at end of file

addons/teach/package.json

+{
+    "name": "@jscoq/teach",
+    "description": "Teach coq",
+    "version": "0.1.0",
+    "files": ["README.md", "coq-pkgs"],
+    "repository": {
+        "type": "git",
+        "url": "https://gitlab.inria.fr/dhamelin/test-jscoq-addon"
+    },
+    "license": "AGPL-3.0-or-later"
+}

addons/teach/teach-pkg.json

+{
+    "rootdir": "workdir",
+    "builddir": "coq-pkgs",
+    "projects": {
+        "teach": {
+            "theories": {
+                "prefix": "Teach"
+            }
+        }
+    }
+}

addons/teach/workdir/.gitignore

+.DS_Store
+.~lock*
+*.swp
+*.aux
+*.fdb_latexmk
+*.fls
+*.log
+*.out
+*.synctex.gz
+*.toc
+*.vrb
+_minted*
+*.nav
+*.snm
+*.vo
+*.vok
+*.vos
+*.glob
+*.bbl
+*.blg
+.*.aux
+.*.cache
+*cache
+.*Makefile.d
+*Makefile*
+coq-num-analysis
+article.pdf

addons/teach/workdir/dune-project

+(lang dune 2.5)
+(using coq 0.2)
+
+(name teach)
\ No newline at end of file

addons/teach/workdir/teach.opam

+opam-version: "2.0"
+version: "8.16.dev"
+build: [
+  [make "-j%{jobs}%"]
+]
+install: [
+  [make "install"]
+]
+depends: [
+  "coq" { >= "8.16~" & < "8.17~" } 
+  "ocamlfind" {build}
+]

addons/teach/workdir/theories/DivPrelude.v

+(**
+This file is part of the coq-teach library
+
+Copyright (C) Boldo, Clément, Hamelin, Mayero, Rousselin
+
+This library is free software; you can redistribute it and/or
+modify it under the terms of the GNU Lesser General Public
+License as published by the Free Software Foundation; either
+version 3 of the License, or (at your option) any later version.
+
+This library is distributed in the hope that it will be useful,
+but WITHOUT ANY WARRANTY; without even the implied warranty of
+MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+COPYING file for more details.
+*)
+
+From Coq.ZArith Require Import BinInt Znumtheory.
+From Coq Require Import Classical.
+From Coq Require Import List.
+Import ListNotations.
+From Teach Require Import Zmod_div Zprime.
+Export Znumtheory(prime).
+
+(** * Preliminary lemmas and types for arithmetics exercises *)
+#[local] Open Scope Z.
+
+(** ** Missing lemmas about modular arithmetics *)
+
+(** ** Numbers as non-empty strings of decimal digits *)
+
+Inductive Digit :=
+  d0 | d1 | d2 | d3 | d4 | d5 | d6 | d7 | d8 | d9.
+
+Definition Z_of_Digit (c : Digit) :=
+match c with
+  d0 => 0
+| d1 => 1
+| d2 => 2
+| d3 => 3
+| d4 => 4
+| d5 => 5
+| d6 => 6
+| d7 => 7
+| d8 => 8
+| d9 => 9
+end.
+
+Inductive Digits :=
+| dsingleton (x : Digit) (* Un seul chiffre | A single digit *)
+| dcons (x : Digit) (xs : Digits). (* Un chiffre suivi d'autres chiffres | A digit followed by other digits *)
+(* Coercion dsingleton : Digit >-> Digits. *)
+
+(*
+⟪ = Ctrl+Shift+u 27EA
+⟫ = Ctrl+Shift+u 27EB
+*)
+Notation "⟪ x ⟫" := (dsingleton x).
+Notation "⟪ x ; .. ; w ; z ⟫" := (dcons x .. (dcons w (dsingleton z)) ..).
+
+(* When compared to List.length, digits_len returns a Z rather than a nat *)
+(* L'avantage par rapport à List.length : on renvoie un Z plutôt qu'un nat *)
+Fixpoint digits_len (l : Digits): Z :=
+  match l with
+  | dsingleton _ => 1
+  | dcons _ xs => (digits_len xs) + 1
+  end.
+
+(* ♯ = Ctrl+Shift+u 266F *)
+Notation "♯ x" := (digits_len x) (at level 40).
+
+Fixpoint digits_sum (cs : Digits) : Z :=
+  match cs with
+  | dsingleton d => Z_of_Digit d
+  | dcons x xs => (Z_of_Digit x) + (digits_sum xs)
+  end.
+
+Fixpoint Z_of_Digits (l : Digits): Z :=
+  match l with
+  | dsingleton d => (Z_of_Digit d)
+  | dcons x xs => (Z_of_Digit x)*10^(♯xs) + (Z_of_Digits xs)
+  end.
+
+Fixpoint shiftr (d : Digits) :=
+  match d with
+  | dsingleton d' => dsingleton d0
+  | dcons h (dsingleton d') => dsingleton h
+  | dcons h t => dcons h (shiftr t)
+  end.
+
+Fixpoint digits_canon (l : Digits) : Digits :=
+  match l with
+  | dcons d0 xs => digits_canon xs
+  | l => l
+  end.
+
+Definition first_digit (xs : Digits) : Digit :=
+  match xs with
+  | dsingleton d => d
+  | dcons x _ => x
+  end.
+
+Fixpoint last_digit (xs : Digits) : Digit :=
+  match xs with
+  | dsingleton d => d
+  | dcons _ xs => last_digit xs
+  end.
+
+Definition findall {E} (P : E -> Prop) :=
+  { l : list E | (Forall P l /\ (forall (x : E), P x -> In x l)) }.
+
+Ltac atomize H := destruct H as [H | H]; [| try atomize H].
+
+Definition not_In {E : Type} (x : E) (l : list E) := ~ In x l.
+
+
+(** ** Missing lemmas about modular arithmetics *)
+Module Z.
+
+(* TODO: Is it really needed ? *)
+Lemma square_opp (x : Z) : (- x) * (- x) = x * x.
+Proof. rewrite Z.mul_opp_opp. reflexivity. Qed.
+
+Lemma le_square_r (k : Z) : k <= k * k.
+Proof.
+  destruct (Z.nonpos_pos_cases k) as [H | H].
+  - apply Z.le_trans with (1 := H); exact (Z.square_nonneg k).
+  - rewrite <-(Z.mul_1_l k) at 1; apply Z.mul_le_mono_pos_r; [exact H |].
+    apply Z.le_succ_l in H; rewrite Z.one_succ; exact H.
+Qed.
+
+Lemma mod_decomp (a b r : Z) (h : a mod b = r) :
+  exists k, a = b * k + r.
+Proof.
+  destruct (Z.eq_dec b 0) as [-> | I].
+  - exists a; rewrite Z.mul_0_l, Z.add_0_l.
+    rewrite Z.mod_0_r in h; rewrite h; reflexivity.
+  - exists (a / b); rewrite <-h; exact (Z.div_mod a b).
+Qed.
+
+Lemma zero_or_ge_1 (n : Z) : n <= - 1 \/ n = 0 \/ 1 <= n.
+Proof.
+  destruct n as [| p | p].
+  - right; left; reflexivity.
+  - right; right; apply Pos2Z.pos_le_pos; exact (Pos.le_1_l p).
+  - left; apply Pos2Z.neg_le_neg; exact (Pos.le_1_l p).
+Qed.
+
+Lemma div_eucl_unique (a b q q' r r' : Z) :
+  b <> 0 -> a = b * q + r -> a = b * q' + r' -> 0 <= r < b -> 0 <= r' < b
+    -> q = q' /\ r = r'.
+Proof.
+  intros bn0 eq eq' ineq ineq'.
+  rewrite eq in eq'.
+  apply Z.add_move_r in eq'; rewrite <-Z.add_sub_assoc in eq'.
+  apply eq_sym, Z.add_move_l in eq'.
+  rewrite <-Z.mul_sub_distr_l in eq'.
+  assert (- b < b * (q - q') < b) as key. {
+    rewrite <-eq'; split.
+    - apply Z.lt_add_lt_sub_l, (Z.lt_le_trans _ 0); [| now apply ineq'].
+      apply Z.lt_add_lt_sub_r; rewrite Z.sub_opp_r, Z.add_0_l; now apply ineq.
+    - apply Z.lt_sub_lt_add_l, (Z.lt_le_trans _ b); [now apply ineq' |].
+      rewrite <-(Z.add_0_l b) at 1; apply Z.add_le_mono_r; now apply ineq.
+  }
+  assert (q - q' = 0) as qq'. {
+    apply Z.abs_lt in key.
+    assert (0 < b) as Ib. {
+      apply Z.le_lt_trans with (2 := key).
+      exact (Z.abs_nonneg _).
+    }
+    rewrite Z.abs_mul, Z.abs_eq in key by (now apply Z.lt_le_incl).
+    apply Z.abs_0_iff.
+    destruct (zero_or_ge_1 (Z.abs (q - q'))) as [I |[-> | I]].
+    - exfalso; apply Z.le_ngt with (1:= Z.abs_nonneg (q - q')).
+      apply Z.le_lt_trans with (1 := I).
+      exact (Pos2Z.neg_is_neg _).
+    - reflexivity.
+    - exfalso; apply Z.lt_nge with (1 := key).
+      apply Z.le_mul_diag_r; [exact Ib | exact I].
+  }
+  rewrite qq', Z.mul_0_r in eq'; split.
+  - now apply Z.sub_move_0_r.
+  - now apply eq_sym, Z.sub_move_0_r.
+Qed.
+(*
+Lemma div_ (a b q r : Z) :
+  b <> 0 -> a = b * q + r -> 0 <= r < b -> q = a / b /\ r = a mod b.
+Proof.
+  intros h1 h2 h3.
+    Search (?a = ?b * ?q + ?r) (?r = ?a mod ?b).
+    Search (?a = ?b * ?q + ?r) (?q = ?a / ?b).
+  pose proof (Z.div_unique_pos a b q r h3 h2) as h4.
+
+  pose proof (
+  split.
+  * 
+*)
+
+Lemma digits_sum_suiv (c : Digit) (cs : Digits) : digits_sum (dcons c cs) = (Z_of_Digit c) + digits_sum cs.
+Proof. reflexivity. Qed.
+
+Lemma Z_of_Digits_dsingleton (d : Digit) :
+  Z_of_Digits (dsingleton d) = Z_of_Digit d.
+Proof. reflexivity. Qed.
+
+Lemma Z_of_Digits_dcons (h : Digit) (t : Digits) :
+  Z_of_Digits (dcons h t) = (Z_of_Digit h) * 10 ^(♯t) + (Z_of_Digits t).
+Proof. reflexivity. Qed.
+
+Lemma shiftr_dsingleton (d : Digit) :
+  shiftr (dsingleton d) = dsingleton d0.
+Proof. reflexivity. Qed.
+
+Lemma shiftr_two_digits (d d' : Digit) :
+  shiftr (dcons d (dsingleton d')) = dsingleton d.
+Proof. reflexivity. Qed.
+
+Lemma shiftr_digits (h h' : Digit) (t : Digits) :
+  shiftr (dcons h (dcons h' t)) = dcons h (shiftr (dcons h' t)).
+Proof. reflexivity. Qed.
+
+Lemma digits_len_digit (d : Digit) : digits_len (dsingleton d) = 1.
+Proof. reflexivity. Qed.
+
+Lemma digits_len_digits (h : Digit) (t : Digits) :
+  digits_len (dcons h t) = (digits_len t) + 1.
+Proof. reflexivity. Qed.
+
+Lemma digits_sum_digit (d : Digit) :
+  digits_sum (dsingleton d) = (Z_of_Digit d).
+Proof. reflexivity. Qed.
+
+Lemma digits_sum_digits (h : Digit) (t : Digits) :
+  digits_sum (dcons h t) = (Z_of_Digit h) + digits_sum t.
+Proof. reflexivity. Qed.
+
+Lemma digits_len_shiftr_digits (h : Digit) (t : Digits) :
+  digits_len (shiftr (dcons h t)) = digits_len t.
+Proof.
+  revert h; induction t as [d | d t' IH].
+  - intros h; rewrite shiftr_two_digits, 2!digits_len_digit; reflexivity.
+  - intros h; rewrite shiftr_digits, 2digits_len_digits, IH; reflexivity.
+Qed.
+
+Lemma digits_len_nneg (d : Digits) : 0 <= digits_len d.
+Proof.
+  induction d as [d | h t IH].
+  - rewrite digits_len_digit; exact (Z.le_0_1).
+  - rewrite digits_len_digits; apply Z.add_nonneg_nonneg;
+      [exact IH | exact Z.le_0_1].
+Qed.
+
+Lemma digits_canon_correct (l : Digits) : Z_of_Digits l = Z_of_Digits (digits_canon l).
+Proof.
+  induction l as [x | h t IH]; [reflexivity |].
+  destruct h; [simpl; exact IH | reflexivity..].
+Qed.
+
+Lemma last_digit_digit (d : Digit) :
+  last_digit (dsingleton d) = d.
+Proof. reflexivity. Qed.
+
+Lemma last_digit_digits (h : Digit) (t : Digits) :
+  last_digit (dcons h t) = last_digit t.
+Proof. reflexivity. Qed.
+
+Lemma decimal_decomposition (n : Digits) :
+  Z_of_Digits n = 10 * (Z_of_Digits (shiftr n)) + (Z_of_Digit (last_digit n)).
+Proof.
+  induction n as [d | h t IH].
+  - reflexivity.
+  - destruct t as [d | h' t'].
+    + rewrite shiftr_two_digits, last_digit_digits, last_digit_digit.
+      rewrite Z_of_Digits_dcons, digits_len_digit, Z.pow_1_r.
+      rewrite !Z_of_Digits_dsingleton, Z.mul_comm; reflexivity.
+    + rewrite shiftr_digits, Z_of_Digits_dcons, digits_len_digits.
+      rewrite (Z_of_Digits_dcons h), last_digit_digits, IH.
+      rewrite digits_len_shiftr_digits, Z.add_assoc; f_equal.
+      rewrite Z.mul_add_distr_l; f_equal.
+      rewrite Z.pow_add_r; [| exact (digits_len_nneg _) | exact Z.le_0_1].
+      rewrite Z.pow_1_r, Z.mul_assoc, Z.mul_comm; reflexivity.
+Qed.
+
+Lemma digits_canon_nonzero (l : Digits) :
+  (digits_canon l) = ⟪ d0 ⟫ \/ first_digit (digits_canon l) <> d0.
+Proof.
+  induction l as [x | h t [IH0 | IHn0]].
+  - destruct x; [left; reflexivity | right; intros H; discriminate H..].
+  - destruct h; [left; simpl; exact IH0 | right; intros H; discriminate H..].
+  - right; destruct h; simpl; [exact IHn0 | intros H; discriminate H..].
+Qed.
+
+Lemma In_dec {E : Type} (x : E) (l : list E) :
+  (In x l) \/ (not_In x l).
+Proof.
+  induction l as [|y l [IH | IH]]; [right; intros [] |..].
+  - left; right; exact IH.
+  - destruct (classic (y = x)) as [-> | H].
+    + left; left; reflexivity.
+    + right; intros [H' | H']; [exact (H H') | exact (IH H')].
+Qed.
+
+Definition primeb_correct := Z.primeb_correct.
+Definition not_prime_0 := not_prime_0.
+Definition pair_equal_spec := pair_equal_spec.
+Definition is_nonneg := Pos2Z.is_nonneg.
+Definition prime_divisors := prime_divisors.
+Definition prime_ge_2 := prime_ge_2.
+Definition add_1_r := Z.add_1_r.
+Definition add_mod := Z.add_mod.
+Definition add_opp_diag_r := Z.add_opp_diag_r.
+Definition divide_0_l := Z.divide_0_l.
+Definition divide_add_cancel_l := Z.divide_add_cancel_l.
+Definition divide_add_cancel_r := Z.divide_add_cancel_r.
+Definition divide_add_r := Z.divide_add_r.
+Definition divide_factor_l := Z.divide_factor_l.
+Definition divide_factor_r := Z.divide_factor_r.
+Definition divide_mul_l := Z.divide_mul_l.
+Definition divide_mul_r := Z.divide_mul_r.
+Definition divide_opp_r := Z.divide_opp_r.
+Definition divide_pos_le := Z.divide_pos_le.
+Definition divide_refl := Z.divide_refl.
+Definition gauss := Z.gauss.
+Definition mod_0_l := Z.mod_0_l.
+Definition mod_divide := Z.mod_divide.
+Definition mul_1_r := Z.mul_1_r.
+Definition mul_assoc := Z.mul_assoc.
+Definition mul_comm := Z.mul_comm.
+Definition mul_mod := Z.mul_mod.
+Definition mul_succ_r := Z.mul_succ_r.
+Definition pow_1_l := Z.pow_1_l.
+Definition pow_m1_l_odd := Z.pow_m1_l_odd.
+Definition pow_mod := Z.pow_mod.
+Definition divide_mul_cancel_l := Z.divide_mul_cancel_l.
+End Z.
+
+(* Tactics *)
+Import Z.
+Fixpoint range_pos (a b : Z) (n: nat) (acc: list Z) {struct n} : list Z :=
+  match n with
+  | O => a :: acc
+  | S n' => range_pos a (b-1) n' (cons b acc)
+  end.
+
+Fixpoint range_neg (a b : Z) (n: nat) (acc: list Z) {struct n} : list Z :=
+  match n with
+  | O => b :: acc
+  | S n' => range_neg (a+1) b n' (cons a acc)
+  end.
+
+Definition range (a b : Z) : list Z :=
+  if a <=? b
+  then range_pos a b (Z.to_nat (b-a)) nil
+  else range_neg b a (Z.to_nat (a-b)) nil
+.
+
+
+#[local]
+Ltac false_solv := match goal with
+| [H : False |- _ ] => destruct H
+end.
+
+#[local]
+Ltac casparcas' H := destruct H as [H | H]; [| try casparcas' H; try false_solv ].
+
+#[local]
+Ltac casparcas x l H :=
+specialize (In_dec x l) as H; unfold In in H; unfold not_In in H; destruct H as [H|H]; [casparcas' H|].
+
+(*Ltac casparcas_range x a b H :=
+specialize (In_dec x (range a b)) as H; remember x as __x' in H; simpl in H; subst __x'; unfold In in H; unfold not_In in H; destruct H as [H|H]; [casparcas' H|]. *)
+
+#[local]
+Ltac casparcas_range x a b H :=
+  specialize (In_dec x (range a b)) as H; remember x as __x' in H; destruct H as [H|H];
+  [ unfold In in H; simpl in H; subst __x'; casparcas' H | unfold not_In in H; simpl in H; subst __x' ].
+
+
+(*
+La tactique `study` est conçue pour rendre plus simple l'analyse des valeurs d'une expression
+Si on a un but de la forme Γ ⊢ G, et une expression E : T, alors on peut utilise la tactique
+`study E in [a_1,a_2,...,a_n] as H` qui génerera (n+1) buts: le premier est:
+
+Γ,H:E <> a1 /\ E <> a2 /\ ... /\ E <> a_n ⊢ G
+Autrement dit, on doit prouver le but quand on sait que l'expression E
+n'est égale à aucun des élements de la liste d'expression qu'on a donné.
+
+Le second but est Γ,H:E = a1 ⊢ G, le troisième Γ,H:E = a2 ⊢ G ... et ainsi de suite jusqu'à Γ,H:E = an ⊢ G
+
+Cette tactique est particulièrement utile dans le contexte des exercices sur la divisibilité, où étudier
+les restes possibles d'une division euclidienne est courant pour prouver certaines propriétés.
+
+~~~~
+
+The study tactic is designed to make it easier to analyse the different possibles values of an expression
+If we have a goal of the form Γ ⊢ G, and an expression E : T, then we can use the tactic
+`study E in [a_1,a_2,...,a_n] as H` to generate (n+1) goals: the first one is
+
+Γ,H:E <> a1 /\ E <> a2 /\ ... /\ E <> a_n ⊢ G : We have to prove the goal when we know that E is not in the list of expression.
+
+The second goal is Γ,H:E = a1 ⊢ G, third is Γ,H:E = a2 ⊢ G and so on until Γ,H:E = an ⊢ G
+
+This tactic is useful in the context of divisibility, where studying the range of remainder is common to
+prove some properties.
+*)
+Tactic Notation "study" constr(x) "in" constr(l) "as" simple_intropattern(H) := casparcas x l H.
+
+(*
+`study E between a and b as H` est un sucre syntaxique pour `study E in [a,a+1,a+2,...,b] as H` (si a <= b) ou `[a,a-1,a-2,...,b]` (si a > b)
+
+Il est courant d'analyser des intervalles continus lorsqu'on travaille sur la divisibilité:
+Ce raccourcis permet d'éviter de faire des erreurs en listant les valeurs possibles d'un intervalle.
+
+~~~
+
+`study E between a and b as H` is a syntax sugar for `study E in [a,a+1,a+2,...,b] as H` (if a <= b) or [a,a-1,a-2,...,b] (if a > b)
+
+It is common to have contiguous ranges when working with divisibility:
+This syntax makes it less error-prone to list all possible values in a range.
+*)
+Tactic Notation "study" constr(x) "between" constr(a) "and" constr(b) "as" simple_intropattern(H) := casparcas_range x a b H.
+
+Add Search Blacklist "Coq".
+
+Require Import Zify.

addons/teach/workdir/theories/Nat_Compl.v

+(**
+This file is part of the coq-teach library
+
+Copyright (C) Boldo, Clément, Hamelin, Mayero, Rousselin
+
+This library is free software; you can redistribute it and/or
+modify it under the terms of the GNU Lesser General Public
+License as published by the Free Software Foundation; either
+version 3 of the License, or (at your option) any later version.
+
+This library is distributed in the hope that it will be useful,
+but WITHOUT ANY WARRANTY; without even the implied warranty of
+MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+COPYING file for more details.
+*)
+
+(** * Additional results on [nat], the type of Peano natural numbers. *)
+
+From Coq Require Import PeanoNat Compare_dec.
+
+
+Local Open Scope nat_scope.
+
+
+Section Nat_eq_Compl.
+
+(** ** Compléments sur l'égalité. / Complements on equality. *)
+
+Lemma nat_neq_0_1 : 0 <> 1.
+Proof. exact (Nat.neq_0_succ 0). Qed.
+
+Lemma nat_eq_1_equiv n : n = 1 <-> n <> 0 /\ n <= 1.
+Proof.
+split.
++ intros; subst; split. apply not_eq_sym, nat_neq_0_1. apply Nat.le_refl.
++ intros [H1 H2]; apply Nat.le_1_r in H2; destruct H2; subst. contradict H1.
+  all: reflexivity.
+Qed.
+
+Lemma nat_pred_neq_0 n : pred n <> 0 <-> n <> 0 /\ n <> 1.
+Proof.
+split.
++ intros H; split; contradict H; subst; reflexivity.
++ intros [H0 H1] H. destruct n. contradict H0; reflexivity.
+  rewrite Nat.pred_succ in H. contradict H1; subst; reflexivity.
+Qed.
+
+End Nat_eq_Compl.
+
+
+Section Nat_ineq_Compl.
+
+(** ** Compléments sur les inégalités. / Complements on inequalities. *)
+
+Lemma nat_le_S_l m n : S m <= n -> m <= n.
+Proof.
+intros H. apply Nat.le_trans with (S m). 2: assumption.
+apply Nat.le_succ_diag_r.
+Qed.
+
+Lemma nat_le_1_S n : 1 <= S n.
+Proof. rewrite <- Nat.succ_le_mono; apply Nat.le_0_l. Qed.
+
+(* "_wnl" means "when (something is) not last", here "when m <> S n". *)
+Lemma nat_le_S_wnl m n : m <= S n -> m <> S n -> m <= n.
+Proof.
+intros H1 H2; apply Nat.nlt_ge; contradict H2.
+apply Nat.le_antisymm. 2: apply Nat.le_succ_l. all: assumption.
+Qed.
+
+(* "_wnl" means "when (something is) not last", here "when m <> n". *)
+Lemma nat_lt_S_wnl m n : m < S n -> m <> n -> m < n.
+Proof.
+intros H1 H2; apply Nat.nle_gt; contradict H2.
+apply Nat.le_antisymm. apply Nat.lt_succ_r. all: assumption.
+Qed.
+
+(* "_wnf" means "when (something is) not first", here "when n <> S m". *)
+Lemma nat_lt_S_wnf m n : m < n -> n <> S m -> S m < n.
+Proof.
+intros H1 H2; apply Nat.nle_gt; contradict H2.
+apply Nat.le_antisymm. 2: apply Nat.le_succ_l. all: assumption.
+Qed.
+
+Lemma nat_S2_gt_1 n : 1 < S (S n).
+Proof.
+induction n. apply Nat.lt_1_2.
+apply Nat.lt_trans with (S (S n)). assumption.
+apply Nat.lt_succ_diag_r.
+Qed.
+
+Lemma nat_lt_le_dec m n : {m < n} + {n <= m}.
+Proof. destruct (le_lt_dec n m). right; assumption. left; assumption. Qed.
+
+End Nat_ineq_Compl.
+
+
+Section Nat_add_Compl.
+
+(** ** Compléments sur l'addition. / Complements on addition. *)
+
+Lemma nat_add_0_r_equiv m n : m = m + n <-> n = 0.
+Proof.
+split; intros H.
++ rewrite <- (Nat.add_0_l n), <- (Nat.sub_diag m) at 1.
+  rewrite <- Nat.add_sub_swap, <- H, Nat.sub_diag.
+  reflexivity. apply Nat.le_refl.
++ subst; apply eq_sym, Nat.add_0_r.
+Qed.
+
+Lemma nat_add_0_l_equiv m n : n = m + n <-> m = 0.
+Proof. rewrite Nat.add_comm. apply nat_add_0_r_equiv. Qed.
+
+Lemma nat_add_S_pred m n : n <> 0 -> S m + pred n = m + n.
+Proof.
+intros; rewrite Nat.add_pred_r, Nat.add_succ_l. 2: assumption.
+apply Nat.pred_succ.
+Qed.
+
+Lemma nat_add_pred_S m n : m <> 0 -> pred m + S n = m + n.
+Proof.
+intros; rewrite Nat.add_pred_l, Nat.add_succ_r. 2: assumption.
+apply Nat.pred_succ.
+Qed.
+
+(* Partial contrapositive of Nat.eq_add_1.
+ "_wn0" means "when (something is) not 0", here "when m <> 0 /\ n <> 0". *)
+Lemma nat_eq_add_1_contra_wn0 m n : m <> 0 -> n <> 0 -> m < n -> m + n <> 1.
+Proof.
+intros H1 H2 H; contradict H1; apply Nat.eq_add_1 in H1.
+destruct H1 as [[Hm Hn] | [Hm Hn]]; subst. contradict H2. all: reflexivity.
+Qed.
+
+(* Partial contrapositive of Nat.eq_add_1.
+ "_wn1" means "when (something is) not 1", here "when n <> 1". *)
+Lemma nat_eq_add_1_contra_wn1 m n : n <> 1 -> m < n -> m + n <> 1.
+Proof.
+intros Hn H; contradict Hn; apply Nat.eq_add_1 in Hn.
+destruct Hn as [[Hm Hn] | [Hm Hn]]; subst. 2: reflexivity.
+contradict H. apply Nat.nlt_ge, Nat.le_0_1.
+Qed.
+
+Lemma nat_lt_add_l_S m n p : m <= p -> m < n + S p.
+Proof. rewrite <- Nat.lt_succ_r; apply Nat.lt_lt_add_l. Qed.
+
+(* "_wn0" means "when (something is) not 0", here "when n <> 0". *)
+Lemma nat_lt_add_l_wn0 m n p : n <> 0 -> m <= p -> m < n + p.
+Proof.
+intros Hn H. rewrite <- (Nat.succ_pred n). 2: assumption.
+rewrite Nat.add_succ_comm. apply nat_lt_add_l_S. assumption.
+Qed.
+
+Lemma nat_add_lt_l_S m n : m + n < m + S n.
+Proof. apply Nat.add_lt_mono_l, Nat.lt_succ_diag_r. Qed.
+
+Lemma nat_lt_add_S m n p : p < m + n -> p < m + S n.
+Proof.
+intros. apply Nat.lt_trans with (m + n). assumption. apply nat_add_lt_l_S.
+Qed.
+
+Lemma nat_le_add_r_lt_S m n : m <= m + n < m + S n.
+Proof. split. apply Nat.le_add_r. apply nat_add_lt_l_S. Qed.
+
+Lemma nat_le_lt_add_S m n p : m <= p < m + n -> m <= p < m + S n.
+Proof. intros [H1 H2]. split. assumption. apply nat_lt_add_S. assumption. Qed.
+
+Lemma nat_lt_add_succ_r m n p : m < n + S p <-> m <= n + p.
+Proof. rewrite <- Nat.lt_succ_r. rewrite Nat.add_succ_r. apply iff_refl. Qed.
+
+Lemma nat_le_lt_add_succ_r m n p : m <= p < m + S n <-> m <= p <= m + n.
+Proof. rewrite nat_lt_add_succ_r. apply iff_refl. Qed.
+
+End Nat_add_Compl.
+
+
+Section Nat_sub_Compl.
+
+(** ** Compléments sur la soustraction. / Complements on subtraction. *)
+
+Lemma nat_sub_0_eq m n : m - n = 0 /\ n - m = 0 <-> m = n.
+Proof.
+rewrite !Nat.sub_0_le; split.
++ intros [H1 H2]; apply Nat.le_antisymm; assumption.
++ intros; subst; split; apply Nat.le_refl.
+Qed.
+
+Lemma nat_sub_S_1 n : S n - 1 = n.
+Proof. rewrite Nat.sub_1_r, Nat.pred_succ. reflexivity. Qed.
+
+Lemma nat_pred_sub m n : pred (m - n) = pred m - n.
+Proof.
+revert m; induction n.
++ intros; rewrite !Nat.sub_0_r. reflexivity.
++ intros; rewrite !Nat.sub_succ_r. rewrite IHn; reflexivity.
+Qed.
+
+Lemma nat_sub2 m n p : p <= n -> n <= m -> m - (n - p) = m - n + p.
+Proof.
+intros H1 H2; apply Nat.add_sub_eq_r.
+rewrite Nat.add_sub_assoc. 2: assumption.
+rewrite <- Nat.add_assoc, (Nat.add_comm p), Nat.add_assoc.
+rewrite <- Nat.add_sub_assoc. 2: apply Nat.le_refl.
+rewrite Nat.sub_diag, Nat.add_0_r.
+apply Nat.sub_add; assumption.
+Qed.
+
+Lemma nat_sub_0_le m n : m <= n -> m - n = 0.
+Proof. intros; apply Nat.sub_0_le; assumption. Qed.
+
+Lemma nat_sub_0_lt m n : m < n -> m - n = 0.
+Proof. intros; apply nat_sub_0_le, Nat.lt_le_incl; assumption. Qed.
+
+Lemma nat_sub_n0_lt m n : m - n <> 0 <-> n < m.
+Proof.
+split. 2: apply Nat.sub_gt.
+intros H; apply Nat.nle_gt. contradict H. apply Nat.sub_0_le; assumption.
+Qed.
+
+Lemma nat_sub_lt_mono_rev m n p q : p <= q -> m - p < n - q -> m < n.
+Proof.
+intros H1 H2. destruct (le_lt_dec q n) as [H3 | H3].
+2: { contradict H2. apply Nat.nlt_ge. replace (n - q) with 0.
+    apply Nat.le_0_l. apply eq_sym, Nat.sub_0_le, Nat.lt_le_incl. assumption. }
+destruct (le_lt_dec p m) as [H4 | H4].
+2: { apply Nat.lt_le_trans with p. assumption.
+    apply Nat.le_trans with q; assumption. }
+specialize (Nat.add_le_lt_mono _ _ _ _ H1 H2).
+rewrite Nat.add_comm. rewrite (Nat.add_comm q).
+rewrite !Nat.sub_add. 2,3: assumption. tauto.
+Qed.
+
+Lemma nat_sub_add_eq_l m n p : n <= m -> m - n = p -> p + n = m.
+Proof.
+revert n p. induction m.
++ intros n p. rewrite Nat.le_0_r. intros Hn; subst.
+  rewrite Nat.sub_diag, Nat.add_0_r. intros; subst. reflexivity.
++ intros n p. destruct n.
+  - intros _; rewrite Nat.sub_0_r, Nat.add_0_r. intros; subst. reflexivity.
+  - rewrite <- Nat.succ_le_mono, Nat.sub_succ.
+    intros H1 H2. rewrite <- (IHm _ _ H1 H2). apply Nat.add_succ_r.
+Qed.
+
+Lemma nat_sub_add_eq_r m n p : n <= m -> m - n = p -> n + p = m.
+Proof. rewrite Nat.add_comm. apply nat_sub_add_eq_l. Qed.
+
+Lemma nat_le_lt_add_sub m n p : m <= p < m + n -> 0 <= p - m < n.
+Proof.
+intros [H1 H2]; split.
++ apply Nat.le_0_l.
++ apply (Nat.add_lt_mono_l _ _ m). rewrite Nat.add_comm.
+  rewrite Nat.sub_add. all: assumption.
+Qed.
+
+End Nat_sub_Compl.
+
+
+Section Nat_mul_Compl.
+
+(** ** Compléments sur la multiplication. / Complements on multiplication. *)
+
+Lemma nat_le_mul_S_l m n : m <= S n * m.
+Proof. apply Nat.le_add_r. Qed.
+
+Lemma nat_le_mul_S_r m n : m <= m * S n.
+Proof. rewrite Nat.mul_comm; apply nat_le_mul_S_l. Qed.
+
+Lemma nat_lt_mul_S_l m n : 0 < m -> 0 < n -> m < S n * m.
+Proof. intros; apply Nat.lt_add_pos_r, Nat.mul_pos_pos; assumption. Qed.
+
+Lemma nat_lt_mul_S_r m n : 0 < m -> 0 < n -> m < m * S n.
+Proof. rewrite Nat.mul_comm; apply nat_lt_mul_S_l. Qed.
+
+Lemma nat_lt_1_mul_pos_sym m n : 1 < m -> 0 < n -> 1 < n * m.
+Proof. rewrite Nat.mul_comm. apply Nat.lt_1_mul_pos. Qed.
+
+End Nat_mul_Compl.
+
+
+Section Nat_div_Compl.
+
+(** ** Compléments sur la division. / Complements on division. *)
+
+Lemma nat_div_mul_sym a b : b <> 0 -> b * a / b = a.
+Proof. rewrite Nat.mul_comm. apply Nat.div_mul. Qed.
+
+Lemma nat_div_mul_eq a b q : b <> 0 -> Nat.divide b a -> q = a / b -> a = b * q.
+Proof.
+intros Hb [p Hp] Hq. subst. rewrite Nat.div_mul. 2: assumption.
+apply Nat.mul_comm.
+Qed.
+
+End Nat_div_Compl.
+
+
+Module Nat.
+
+Import PeanoNat.Nat.
+
+(** ** Some results from Nat.Div0 and Nat.Lcm0
+
+ These are mostly lemmas taking advantage of the fact that
+ [forall (a : nat), a / 0 = 0 /\ a mod 0 = a]
+ This really makes proofs simpler.
+
+ These lemmas are not available in Coq 8.16 and anyway it is better to mask
+ the corresponding lemmas in PeanoNat.Nat. *)
+
+(* Not available in 8.16. *)
+Lemma mod_0_r (a : nat) : a mod 0 = a.
+Proof. reflexivity. Qed.
+
+(* Not available in 8.16. *)
+Lemma div_0_r (a : nat) : a / 0 = 0.
+Proof. reflexivity. Qed.
+
+(* Not available in 8.16, better than Nat.div_mod, alternative div_mod_eq. *)
+Lemma div_mod (a b : nat) : a = b * (a / b) + a mod b.
+Proof. exact (div_mod_eq a b). Qed.
+
+(* Better than Nat.mod_eq. *)
+Lemma mod_eq (a b : nat) : a mod b = a - b * (a / b).
+Proof.
+  symmetry; apply Nat.add_sub_eq_l; rewrite <-div_mod; reflexivity.
+Qed.
+
+(* Better than Nat.mod_same. *)
+Lemma mod_same (a : nat) : a mod a = 0.
+Proof.
+  rewrite mod_eq; destruct (Nat.eq_dec a 0) as [-> | nE]; [reflexivity |].
+  rewrite (div_same a nE), Nat.mul_1_r, Nat.sub_diag; reflexivity.
+Qed.
+
+(* Better than Nat.mod_mul. *)
+Lemma mod_mul (a b : nat) : a * b mod b = 0.
+Proof.
+  destruct (Nat.eq_dec b 0) as [-> | nE].
+  - rewrite Nat.mul_0_r, mod_0_r; reflexivity.
+  - rewrite mod_eq, (div_mul a b nE), Nat.mul_comm, Nat.sub_diag; reflexivity.
+Qed.
+
+Lemma mod_le (a b : nat) : a mod b <= a.
+Proof. rewrite mod_eq; now apply (Nat.le_sub_l). Qed.
+
+Lemma div_le_mono (a b c : nat) : a <= b -> a / c <= b / c.
+Proof.
+  destruct (Nat.eq_dec c 0) as [-> | nE%Nat.neq_0_lt_0].
+  - intros _; rewrite 2!div_0_r; exact (Nat.le_refl 0).
+  - intros [I | ->]%Nat.le_lteq; [| exact (Nat.le_refl _)].
+    apply ->Nat.lt_succ_r; apply (Nat.mul_lt_mono_pos_l c _ _ nE).
+    rewrite Nat.mul_succ_r.
+    apply (Nat.add_lt_mono_r _ _ (a mod c)); rewrite <-div_mod.
+    apply Nat.lt_trans with (1 := I); rewrite (div_mod b c) at 1.
+    rewrite <-Nat.add_assoc; apply Nat.add_lt_mono_l.
+    apply Nat.lt_lt_add_r, Nat.mod_upper_bound, Nat.neq_0_lt_0; exact nE.
+Qed.
+
+Lemma mul_div_le (a b : nat) : b * (a / b) <= a.
+Proof. rewrite (div_mod a b) at 2; exact (Nat.le_add_r _ _). Qed.
+
+Lemma div_exact (a b : nat) : (a = b * (a / b)) <-> a mod b = 0.
+Proof.
+  rewrite (div_mod a b) at 1; rewrite <-(Nat.add_0_r (b * (a / b))) at 2.
+  exact (add_cancel_l _ _ _).
+Qed.
+
+(* Replaces divide_div_mul_exact, alternative is Lcm0.divide_div_mul_exact. *)
+Lemma divide_div_mul_exact (a b c : nat) :
+  divide b a -> c * a / b = c * (a / b).
+Proof.
+destruct (eq_dec b 0) as [-> | Hb].
+  - intros ->%divide_0_l. rewrite 2!div_0_r, mul_0_r; reflexivity.
+  - intros [q ->]; rewrite mul_assoc, 2!div_mul by (exact Hb); reflexivity.
+Qed.
+
+(* Replaces div_mul_cancel_l, alternative is Div0.div_mul_cancel_l. *)
+Lemma div_mul_cancel_l (a b c : nat) : c <> 0 -> c * a / (c * b) = a / b.
+Proof.
+  destruct (eq_dec b 0) as [-> | nE].
+  - rewrite mul_0_r, 2!div_0_r; intros _; reflexivity.
+  - intros H%neq_0_lt_0; symmetry; apply (div_unique _ _ _ (c * (a mod b))).
+    + apply mul_lt_mono_pos_l; [exact H | exact (mod_upper_bound _ _ nE)].
+    + rewrite (div_mod_eq a b) at 1; rewrite mul_add_distr_l, !mul_assoc;
+        reflexivity.
+Qed.
+
+(* Replaces mod_divide, alternative is Lcm0.mod_divide. *)
+Lemma mod_divide (a b : nat) : a mod b = 0 <-> divide b a.
+Proof.
+  pose proof (div_mod_eq a b); split.
+  - intros E; rewrite E, add_0_r, mul_comm in H; exists (a / b); exact H.
+  - destruct (eq_dec b 0) as [-> | I%neq_0_lt_0].
+    + intros ->%divide_0_l; rewrite mod_0_r; reflexivity.
+    + intros [q Hq]; rewrite <-(add_0_r (q * b)) in Hq.
+      rewrite mul_comm in Hq; apply mod_unique, eq_sym in Hq;
+        [exact Hq | exact I].
+Qed.
+
+End Nat.
+
+
+Section Nat2_Compl.
+
+(** Compléments sur [nat * nat]. / Complements on [nat * nat]. *)
+
+(* Principe d'induction double. / Double induction principle. *)
+Lemma nat_ind2 (P : nat -> nat -> Prop) :
+  P 0 0 ->
+  (forall m n, P m n -> P (S m) n) ->
+  (forall m n, P m n -> P m (S n)) ->
+  forall m n, P m n.
+Proof.
+intros H00 HSl HSr; induction m; intros n.
++ induction n. assumption. apply HSr; assumption.
++ apply HSl, IHm.
+Qed.
+
+(* Principe d'induction double pour une propriété symétrique. /
+ Double induction principle for a symmetric property. *)
+Lemma nat_ind2_sym (P : nat -> nat -> Prop) :
+  (forall m n, P m n -> P n m) ->
+  P 0 0 ->
+  (forall m n, P m n -> P (S m) n) ->
+  forall m n, P m n.
+Proof.
+intros HP P00 HS; apply nat_ind2.
++ assumption.
++ assumption.
++ intros; apply HP, HS, HP; assumption.
+Qed.
+
+(* Décidabilité de deux égalités. / Decidability of two equalities. *)
+Lemma nat_eq2_dec (m1 n1 m2 n2 : nat) :
+  { m1 = n1 /\ m2 = n2 } + { m1 <> n1 \/ m2 <> n2 }.
+Proof.
+destruct (Nat.eq_dec m1 n1) as [H1 | H1].
+destruct (Nat.eq_dec m2 n2) as [H2 | H2].
++ left; split; assumption.
++ right; right; assumption.
++ right; left; assumption.
+Qed.
+
+(* Décidabilité d'une égalité et d'une inégalité (large). /
+ Decidability of an equality and a (large) inequality. *)
+Lemma nat_eq_le2_dec (m1 n1 m2 n2 : nat) :
+  { m1 = n1 /\ m2 <= n2 } + { m1 <> n1 \/ n2 < m2 }.
+Proof.
+destruct (Nat.eq_dec m1 n1) as [H1 | H1].
+destruct (le_lt_dec m2 n2) as [H2 | H2].
++ left; split; assumption.
++ right; right; assumption.
++ right; left; assumption.
+Qed.
+
+(* Décidabilité d'une égalité et d'une inégalité (stricte). /
+ Decidability of an equality and a (strict) inequality. *)
+Lemma nat_eq_l2t_dec (m1 n1 m2 n2 : nat) :
+  { m1 = n1 /\ m2 < n2 } + { m1 <> n1 \/ n2 <= m2 }.
+Proof.
+destruct (Nat.eq_dec m1 n1) as [H1 | H1].
+destruct (nat_lt_le_dec m2 n2) as [H2 | H2].
++ left; split; assumption.
++ right; right; assumption.
++ right; left; assumption.
+Qed.
+
+End Nat2_Compl.

addons/teach/workdir/theories/Nat_Factorial.v

+(**
+This file is part of the coq-teach library
+
+Copyright (C) Boldo, Clément, Hamelin, Mayero, Rousselin
+
+This library is free software; you can redistribute it and/or
+modify it under the terms of the GNU Lesser General Public
+License as published by the Free Software Foundation; either
+version 3 of the License, or (at your option) any later version.
+
+This library is distributed in the hope that it will be useful,
+but WITHOUT ANY WARRANTY; without even the implied warranty of
+MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+COPYING file for more details.
+*)
+
+(** * Support for factorials in [nat], the type of Peano natural numbers. *)
+
+From Coq Require Import PeanoNat Compare_dec.
+
+From Teach Require Import Nat_Compl.
+
+
+Local Open Scope nat_scope.
+
+
+Section Fact_Def.
+
+(* Factorielle de n. / Factorial of n.
+ fact n = 1 * 2 * ... * (n - 1) * n. *)
+Fixpoint fact (n : nat) : nat :=
+  match n with
+  | O => 1
+  | S n' => fact n' * S n'
+  end.
+
+End Fact_Def.
+
+
+Section Fact_Facts.
+
+Lemma fact_0 : fact 0 = 1.
+Proof. reflexivity. Qed.
+
+Lemma fact_1 : fact 1 = 1.
+Proof. reflexivity. Qed.
+
+Lemma fact_S n : fact (S n) = fact n * S n.
+Proof. reflexivity. Qed.
+
+Lemma fact_pred n : fact n = fact (S n) / S n.
+Proof. rewrite fact_S, Nat.div_mul. reflexivity. discriminate. Qed.
+
+Lemma fact_gt_0 n : 0 < fact n.
+Proof.
+induction n. apply Nat.lt_0_1.
+rewrite fact_S; apply Nat.mul_pos_pos. apply IHn. apply Nat.lt_0_succ.
+Qed.
+
+Lemma fact_neq_0 n : fact n <> 0.
+Proof. apply Nat.neq_0_lt_0, fact_gt_0. Qed.
+
+Lemma fact_mul_neq_0 m n : fact m * fact n <> 0.
+Proof. apply Nat.neq_mul_0; split; apply fact_neq_0. Qed.
+
+Lemma fact_mul2_neq_0 m n p : fact m * fact n * fact p <> 0.
+Proof. apply Nat.neq_mul_0; split. apply fact_mul_neq_0. apply fact_neq_0. Qed.
+
+Lemma fact_S_div n : fact (S n) / fact n = S n.
+Proof. rewrite fact_S. apply nat_div_mul_sym, fact_neq_0. Qed.
+
+Lemma fact_S_div_alt n : 0 < n -> fact n / fact (pred n) = n.
+Proof.
+intros Hn; rewrite <- (Nat.succ_pred n). apply fact_S_div.
+apply Nat.neq_0_lt_0; assumption.
+Qed.
+
+Lemma fact_gt_1 n : 1 < n -> 1 < fact n.
+Proof.
+destruct n. easy.
+intros; rewrite fact_S; apply nat_lt_1_mul_pos_sym. assumption.
+apply fact_gt_0.
+Qed.
+
+Lemma fact_eq_1_equiv n : fact n = 1 <-> n = 0 \/ n = 1.
+Proof.
+apply iff_sym; split.
++ intros [Hn | Hn]; subst. apply fact_0. apply fact_1.
++ destruct (lt_dec 1 n) as [Hn | Hn]; intros Hn1.
+  - contradict Hn1. apply not_eq_sym, Nat.lt_neq, fact_gt_1. assumption.
+  - apply Nat.le_1_r. apply Nat.nlt_ge. assumption.
+Qed.
+
+(* "_wn1" means "when (something is) not 1", here "when n <> 1". *)
+Lemma fact_eq_1_wn1 n : n <> 1 -> fact n = 1 -> n = 0.
+Proof.
+intros H1; rewrite fact_eq_1_equiv; intros [H2 | H2]; subst. 2: contradict H1.
+all: reflexivity.
+Qed.
+
+Lemma fact_le m n : m <= n -> fact m <= fact n.
+Proof.
+intros H; induction H as [| n H IH]. apply Nat.le_refl.
+rewrite fact_S. apply Nat.le_trans with (fact n). assumption.
+apply nat_le_mul_S_r.
+Qed.
+
+(* "_w0" means "when (something is) 0", here "when m = 0". *)
+Lemma fact_lt_w0 m n : m = 0 -> n <> 1 -> m < n -> fact m < fact n.
+Proof.
+intros H0 H1 H; subst. rewrite fact_0; apply fact_gt_1.
+apply Nat.nle_gt. contradict H1. apply Nat.le_antisymm. assumption.
+apply Nat.le_succ_l. assumption.
+Qed.
+
+Lemma fact_lt_S n : n <> 0 -> fact n < fact (S n).
+Proof.
+intros Hn. rewrite fact_S. apply nat_lt_mul_S_r. apply fact_gt_0.
+apply Nat.neq_0_lt_0. assumption.
+Qed.
+
+(* "_wn0" means "when (something is) not 0", here "when m <> 0". *)
+Lemma fact_lt_wn0 m n : m <> 0 -> m < n -> fact m < fact n.
+Proof.
+intros Hm H; induction H as [| n H IH]. apply fact_lt_S; assumption.
+apply Nat.lt_trans with (fact n). assumption.
+apply fact_lt_S. apply Nat.neq_0_lt_0, Nat.le_lt_trans with m.
++ apply Nat.le_0_l.
++ apply Nat.lt_le_trans with (S m). 2: assumption.
+  apply Nat.lt_succ_diag_r.
+Qed.
+
+Lemma fact_lt m n : m + n <> 1 -> m < n -> fact m < fact n.
+Proof.
+intros H; destruct (Nat.eq_dec m 0).
++ subst. apply fact_lt_w0. reflexivity. assumption.
++ apply fact_lt_wn0. assumption.
+Qed.
+
+(* "_w0" means "when (something is) 0", here "when m * n = 0". *)
+Lemma fact_inj_w0 m n : m * n = 0 -> m + n <> 1 -> fact m = fact n -> m = n.
+Proof.
+rewrite Nat.mul_eq_0. intros [Hm | Hn]; subst; rewrite fact_0.
++ intros. rewrite fact_eq_1_wn1; easy.
++ rewrite Nat.add_0_r. apply fact_eq_1_wn1.
+Qed.
+
+(* "_w0" means "when (something is) 0", here "when m * n <> 0". *)
+Lemma fact_inj_wn0 m n : m <> 0 -> n <> 0 -> fact m = fact n -> m = n.
+Proof.
+intros Hm Hn H1. destruct (Nat.eq_dec m n) as [| H2]. assumption.
+apply not_eq in H2. contradict H1. destruct H2 as [H | H].
++ apply Nat.lt_neq, fact_lt. apply nat_eq_add_1_contra_wn0. all: assumption.
++ apply not_eq_sym, Nat.lt_neq, fact_lt. apply nat_eq_add_1_contra_wn0.
+  all: assumption.
+Qed.
+
+Lemma fact_inj m n : m + n <> 1 -> fact m = fact n -> m = n.
+Proof.
+intros H1. destruct (Nat.eq_dec (m * n) 0) as [H0 | H0].
++ apply fact_inj_w0; assumption.
++ apply Nat.neq_mul_0 in H0. destruct H0 as [Hm Hn].
+  apply fact_inj_wn0; assumption.
+Qed.
+
+Lemma fact_mod_0 m n : m <= n -> (fact n) mod (fact m) = 0.
+Proof.
+intros H. apply Nat.mod_divide.
+revert m H. induction n as [| n IHn].
++ intros m H. apply Nat.le_0_r in H. subst. exists 1. reflexivity.
++ intros m [H | ->]%Nat.le_lteq; [| exact (Nat.divide_refl _)].
+  apply ->Nat.lt_succ_r in H; apply IHn in H.
+  apply Nat.divide_trans with (1 := H).
+  exists (S n); rewrite fact_S, Nat.mul_comm; reflexivity.
+Qed.
+
+Lemma fact_divide n p : S p <= n -> Nat.divide (S p) (fact n).
+Proof.
+intros H1; induction n. contradict H1; apply Nat.nle_succ_0.
+rewrite fact_S. destruct (le_lt_dec (S p) n) as [H2 | H2].
++ apply Nat.divide_mul_l. apply IHn. assumption.
++ replace (S p) with (S n). apply Nat.divide_factor_r.
+  apply Nat.le_antisymm. 2: assumption.
+  apply Nat.le_succ_l. assumption.
+Qed.
+
+End Fact_Facts.

addons/teach/workdir/theories/Nat_Sum.v

+(**
+This file is part of the coq-teach library
+
+Copyright (C) Boldo, Clément, Hamelin, Mayero, Rousselin
+
+This library is free software; you can redistribute it and/or
+modify it under the terms of the GNU Lesser General Public
+License as published by the Free Software Foundation; either
+version 3 of the License, or (at your option) any later version.
+
+This library is distributed in the hope that it will be useful,
+but WITHOUT ANY WARRANTY; without even the implied warranty of
+MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+COPYING file for more details.
+*)
+
+(** * Support for iterated summations in [nat], the type of Peano natural
+ numbers. *)
+
+(* Strong induction is needed. *)
+From Coq Require Import PeanoNat Wf_nat Compare_dec.
+
+From Teach Require Import Nat_Compl.
+
+
+Local Open Scope nat_scope.
+
+
+Section Sum_Def.
+
+(* Somme de n termes à partir de a. / Sum of n terms from a.
+ sum_n a n f = f a + f (a + 1) + ... + f (a + n - 1).
+ n = 0 -> sum_n a n f = 0. *)
+Fixpoint sum_n (a n : nat) (f : nat -> nat) : nat :=
+  match n with
+  | O => 0
+  | S n' => sum_n a n' f + f (a + n')
+  end.
+(*
+Definition sum_range (a b : nat) (f: nat -> nat) := sum_n a (S b-a) f.
+*)
+(* Somme de a à b inclus. / Sum from a to b included.
+ sum_range a b f = f a + f (a + 1) + ... + f (b - 1) + f b.
+ b < a -> sum_range a b f = 0. *)
+Definition sum_range (a b : nat) (f : nat -> nat) : nat :=
+  if le_lt_dec a b then sum_n a (b - a + 1) f else 0.
+
+Definition sum_range_bis (a b : nat) (f: nat -> nat) : nat := sum_n a (S b - a) f.
+
+Lemma sum_range_correct_l a b f :
+  a <= b -> sum_range a b f = sum_n a (b - a + 1) f.
+Proof.
+intros H; unfold sum_range. destruct (le_lt_dec _ _). reflexivity.
+contradict H. apply Nat.nle_gt; assumption.
+Qed.
+
+Lemma sum_range_correct_r a b f : b < a -> sum_range a b f = 0.
+Proof.
+intros H; unfold sum_range. destruct (le_lt_dec _ _). 2: reflexivity.
+contradict H. apply Nat.nlt_ge; assumption.
+Qed.
+
+Lemma sum_n_eq a n f : 0 < a + n -> sum_n a n f = sum_range a (a + n - 1) f.
+Proof.
+intros H. destruct (Nat.eq_dec n 0) as [Hn | Hn].
++ subst. rewrite sum_range_correct_r. reflexivity.
+  rewrite Nat.add_0_r in *. rewrite Nat.sub_1_r.
+  apply Nat.lt_pred_l. apply Nat.neq_0_lt_0. assumption.
++ assert (Hn1 : 1 <= n). apply Nat.le_succ_l, Nat.neq_0_lt_0. assumption.
+  assert (H1 : a <= a + n - 1).
+    rewrite <- Nat.add_sub_assoc. apply Nat.le_add_r. assumption.
+  rewrite sum_range_correct_l. 2: assumption.
+  replace (_ + 1) with n. reflexivity.
+  rewrite <- Nat.add_sub_swap. 2: assumption.
+  rewrite <- (Nat.add_sub_assoc a). 2: assumption.
+  rewrite <- Nat.add_assoc. rewrite Nat.sub_add. 2: assumption.
+  rewrite Nat.add_comm. rewrite Nat.add_sub. reflexivity.
+Qed.
+
+Lemma sum_range_0_l n f : sum_range 0 n f = sum_n 0 (S n) f.
+Proof.
+rewrite sum_range_correct_l. 2: apply Nat.le_0_l.
+rewrite Nat.sub_0_r, Nat.add_1_r. reflexivity.
+Qed.
+
+End Sum_Def.
+
+
+Section Sum_Facts.
+
+Lemma sum_n_ext a n f1 f2 :
+  (forall k, a <= k < a + n -> f1 k = f2 k) -> sum_n a n f1 = sum_n a n f2.
+Proof.
+intro H. induction n. reflexivity.
+simpl. rewrite IHn.
++ rewrite H. reflexivity. apply nat_le_add_r_lt_S.
++ intros k Hk. apply H. apply nat_le_lt_add_S. assumption.
+Qed.
+
+Lemma sum_range_ext a b f1 f2 :
+  (forall k, a <= k <= b -> f1 k = f2 k) -> sum_range a b f1 = sum_range a b f2.
+Proof.
+destruct (le_lt_dec a b) as [H | H].
++ intros Hf. rewrite !sum_range_correct_l. 2,3: assumption.
+  apply sum_n_ext. intros k [Hk1 Hk2]. apply Hf. split. assumption.
+  revert Hk2. rewrite Nat.add_1_r. rewrite Nat.add_succ_r, Nat.lt_succ_r.
+  rewrite Nat.add_comm. rewrite Nat.sub_add. easy. assumption.
++ intros _. rewrite !sum_range_correct_r. reflexivity. all: assumption.
+Qed.
+
+Lemma sum_n_0 a f : sum_n a 0 f = 0.
+Proof. reflexivity. Qed.
+
+Lemma sum_n_1 a f : sum_n a 1 f = f a.
+Proof. unfold sum_n. rewrite Nat.add_0_l, Nat.add_0_r. reflexivity. Qed.
+
+(* (S n) est le successeur de n, c'est-à-dire (n + 1). /
+ (S n) is the successor of n, ie (n + 1). *)
+Lemma sum_n_ind_r a n f : sum_n a (S n) f = sum_n a n f + f (a + n).
+Proof. reflexivity. Qed.
+
+Lemma sum_n_ind_l a n f : sum_n a (S n) f = f a + sum_n (S a) n f.
+Proof.
+revert a.
+apply (lt_wf_ind n).
+clear n. 
+intros n IHn a. rewrite sum_n_ind_r. destruct n.
++ rewrite !Nat.add_0_r. reflexivity.
++ rewrite IHn. 2: apply Nat.lt_succ_diag_r.
+  rewrite sum_n_ind_r. rewrite Nat.add_succ_comm, Nat.add_assoc. reflexivity.
+Qed.
+
+Lemma sum_n_ind (P : nat -> Prop) a n f :
+  P 0 -> (forall i j, P i -> P j -> P (i + j)) ->
+  (forall i, a <= i < a + n -> P (f i)) ->
+  P (sum_n a n f).
+Proof.
+intros HP0 HP Hf. induction n.
++ rewrite sum_n_0. assumption.
++ rewrite sum_n_ind_r. apply HP.
+  - apply IHn. intros i Hi. apply Hf. apply nat_le_lt_add_S. assumption.
+  - apply Hf. apply nat_le_add_r_lt_S.
+Qed.
+
+Lemma sum_n_concat a n1 n2 f :
+  sum_n a n1 f + sum_n (a + n1) n2 f = sum_n a (n1 + n2) f.
+Proof.
+revert a n2 f; induction n1.
++ intros. rewrite sum_n_0, Nat.add_0_l. f_equal. easy.
++ intros a n2 f. rewrite Nat.add_succ_comm. rewrite <- IHn1.
+  rewrite sum_n_ind_r. rewrite sum_n_ind_l. rewrite Nat.add_succ_r.
+  apply eq_sym, Nat.add_assoc.
+Qed.
+
+Lemma sum_n_split m n a f :
+  m <= n -> sum_n a n f = sum_n a m f + sum_n (a + m) (n - m) f.
+Proof.
+intros H. rewrite sum_n_concat. rewrite Nat.add_comm. rewrite Nat.sub_add.
+reflexivity. assumption.
+Qed.
+
+Lemma sum_n_extract i a n f :
+  i < n -> sum_n a n f = sum_n a i f + f (a + i) + sum_n (a + S i) (n - S i) f.
+Proof.
+intros Hi. rewrite (sum_n_split i). 2: apply Nat.lt_le_incl; assumption.
+rewrite <- Nat.add_assoc. f_equal.
+rewrite Nat.add_succ_r. rewrite <- sum_n_ind_l. f_equal.
+rewrite Nat.sub_succ_r. rewrite Nat.succ_pred. reflexivity.
+apply Nat.sub_gt. assumption.
+Qed.
+
+Lemma sum_n_le a n f g :
+  (forall i, a <= i < a + n -> f i <= g i) -> sum_n a n f <= sum_n a n g.
+Proof.
+intros H. induction n.
++ rewrite !sum_n_0. apply Nat.le_refl.
++ rewrite !sum_n_ind_r. apply Nat.add_le_mono. 2: apply H, nat_le_add_r_lt_S.
+  apply IHn. intros i Hi. apply H. apply nat_le_lt_add_S. assumption.
+Qed.
+
+Lemma sum_n_lt a n f g :
+  (forall i, a <= i < a + n -> f i <= g i) ->
+  (exists i, a <= i < a + n /\ f i < g i) ->
+  sum_n a n f < sum_n a n g.
+Proof.
+revert a f g. induction n; intros a f g H1 [i [Hi H2]].
++ destruct Hi as [Hi1 Hi2]. contradict Hi2.
+  rewrite Nat.add_0_r. apply Nat.nlt_ge. assumption.
++ rewrite (sum_n_extract (i - a) _ _ f), (sum_n_extract (i - a) _ _ g).
+  2,3: apply nat_le_lt_add_sub; assumption.
+  destruct Hi as [Hi1 Hi2]. apply Nat.add_lt_le_mono.
+  2: { apply sum_n_le. intros j [Hj1 Hj2]. apply H1. split.
+    + apply Nat.le_trans with (a + S (i - a)). apply Nat.le_add_r. assumption.
+    + apply Nat.lt_le_trans with (a + S (i - a) + (S n - S (i - a))). assumption.
+      rewrite Nat.sub_succ. rewrite <- Nat.add_assoc. rewrite Nat.add_succ_l.
+      rewrite (Nat.add_comm (i - a)). rewrite Nat.sub_add. apply Nat.le_refl.
+      apply Nat.le_sub_le_add_l. apply nat_lt_add_succ_r. assumption. }
+  apply Nat.add_le_lt_mono.
+  2: { replace (a + (i - a)) with i. assumption.
+    rewrite Nat.add_comm. rewrite Nat.sub_add. reflexivity. assumption. }
+  apply sum_n_le. intros j [Hj1 Hj2]. apply H1. split. assumption.
+  apply Nat.lt_trans with i. 2: assumption.
+  rewrite <- (Nat.sub_add a i). 2: assumption.
+  rewrite Nat.add_comm. assumption.
+Qed.
+
+Lemma sum_n_eq_0 a n f :
+  (forall i, a <= i < a + n -> f i = 0) -> sum_n a n f = 0.
+Proof.
+intros H. apply trans_eq with (sum_n a n (fun _ => 0)).
++ apply sum_n_ext. assumption.
++ clear; revert a; induction n. reflexivity.
+  intros a; rewrite sum_n_ind_l. rewrite IHn. reflexivity.
+Qed.
+
+Lemma sum_range_eq_0 a b f :
+  (forall i, a <= i <= b -> f i = 0) -> sum_range a b f = 0.
+Proof.
+intros Hf. destruct (le_lt_dec a b) as [H | H].
+2: { apply sum_range_correct_r. assumption. }
+rewrite sum_range_correct_l. 2: assumption.
+apply sum_n_eq_0. intros i [Hi1 Hi2]. apply Hf. split. assumption.
+apply Nat.lt_succ_r. replace (S b) with (a + (b - a + 1)). assumption.
+rewrite Nat.add_1_r. rewrite <- Nat.sub_succ_l. 2: assumption.
+rewrite Nat.add_comm. rewrite Nat.sub_add. reflexivity.
+apply Nat.le_trans with b. assumption. apply Nat.le_succ_diag_r.
+Qed.
+
+Lemma sum_n_eq_0_rev a n f :
+  sum_n a n f = 0 -> forall i, a <= i < a + n -> f i = 0.
+Proof.
+induction n.
++ rewrite Nat.add_0_r. intros _ i [Hi1 Hi2].
+  contradict Hi1. apply Nat.nle_gt. assumption.
++ rewrite sum_n_ind_r. rewrite Nat.eq_add_0.
+  intros [H1 H2] i Hi1. destruct (Nat.eq_dec i (a + n)) as [Hi2 | Hi2].
+  - subst. assumption.
+  - apply IHn. assumption.
+    destruct Hi1 as [Hi1a Hi1b]. split. assumption.
+    apply nat_lt_S_wnl. 2: assumption.
+    rewrite <- Nat.add_succ_r. assumption.
+Qed.
+
+Lemma sum_n_eq_0_equiv a n f :
+  sum_n a n f = 0 <-> forall i, a <= i < a + n -> f i = 0.
+Proof. split. apply sum_n_eq_0_rev. apply sum_n_eq_0. Qed.
+
+Lemma sum_n_neq_0 a n f :
+  (exists i, a <= i < a + n /\ f i <> 0) -> sum_n a n f <> 0.
+Proof.
+intros [i [Hi Hf]]. contradict Hf.
+apply (sum_n_eq_0_rev a n). all: assumption.
+Qed.
+
+Lemma sum_n_add a n f g :
+  sum_n a n f + sum_n a n g = sum_n a n (fun i => f i + g i).
+Proof.
+induction n. reflexivity.
+rewrite !sum_n_ind_r. rewrite <- IHn. rewrite 2!Nat.add_assoc. f_equal.
+rewrite <- Nat.add_assoc. rewrite (Nat.add_comm (f _)). apply Nat.add_assoc.
+Qed.
+
+Lemma sum_n_sub a n f g :
+  (forall i, a <= i < a + n -> g i <= f i) ->
+  sum_n a n f - sum_n a n g = sum_n a n (fun i => f i - g i).
+Proof.
+intros H. induction n. reflexivity.
+rewrite !sum_n_ind_r. rewrite <- IHn.
+2: { intros i Hi. apply H. apply nat_le_lt_add_S. assumption. }
+rewrite Nat.sub_add_distr. rewrite Nat.add_sub_assoc.
+2: { apply H. apply nat_le_add_r_lt_S. }
+rewrite Nat.add_sub_swap.
+2: { apply sum_n_le. intros i Hi. apply H. apply nat_le_lt_add_S. assumption. }
+reflexivity.
+Qed.
+
+Lemma sum_n_mul_add_distr_l a n f c :
+  c * sum_n a n f = sum_n a n (fun i => c * f i).
+Proof.
+induction n. apply Nat.mul_0_r.
+rewrite !sum_n_ind_r. rewrite <- IHn. apply Nat.mul_add_distr_l.
+Qed.
+
+Lemma sum_n_mul_add_distr_r a n f c :
+  sum_n a n f * c = sum_n a n (fun i => f i * c).
+Proof.
+rewrite Nat.mul_comm. rewrite sum_n_mul_add_distr_l.
+apply sum_n_ext. intros; apply Nat.mul_comm.
+Qed.
+
+Lemma sum_n_shift_l t a n f :
+  t <= a -> sum_n a n f = sum_n (a - t) n (fun i => f (i + t)).
+Proof.
+intros Ht. induction n. reflexivity.
+rewrite !sum_n_ind_r. rewrite IHn.
+replace (a - t + n + t) with (a + n). reflexivity.
+rewrite (Nat.add_comm (a - t)). rewrite <- Nat.add_assoc.
+rewrite Nat.sub_add. 2: assumption.
+apply Nat.add_comm.
+Qed.
+
+Lemma sum_n_shift_r t a n f :
+  sum_n a n f = sum_n (a + t) n (fun i => f (i - t)).
+Proof.
+rewrite (sum_n_shift_l t (a + t)). 2: apply Nat.le_add_l.
+rewrite Nat.add_sub. apply sum_n_ext.
+intros. rewrite Nat.add_sub. reflexivity.
+Qed.
+
+Lemma sum_n_reverse a n f :
+  sum_n a n f = sum_n a n (fun i => f (2 * a + n - 1 - i)).
+Proof.
+induction n. rewrite !sum_n_0; reflexivity.
+rewrite sum_n_ind_r, sum_n_ind_l, (sum_n_shift_l 1 (S a)). 2: apply nat_le_1_S.
+rewrite nat_sub_S_1. replace (_ - a) with (a + n).
+2: { rewrite <- Nat.double_twice, <- Nat.add_sub_assoc. 2: apply nat_le_1_S.
+  unfold Nat.double. rewrite nat_sub_S_1, (Nat.add_comm (_ + _)).
+  rewrite <- Nat.add_sub_assoc. 2: apply Nat.le_add_r.
+  rewrite Nat.add_sub. apply Nat.add_comm. }
+rewrite Nat.add_comm. f_equal. rewrite IHn. apply sum_n_ext.
+intros i Hi. f_equal. rewrite (Nat.add_comm i), Nat.sub_add_distr.
+do 2 f_equal. rewrite <- Nat.add_sub_assoc. 2: apply nat_le_1_S.
+rewrite nat_sub_S_1. reflexivity.
+Qed.
+
+End Sum_Facts.

addons/teach/workdir/theories/Pos_Compl.v

+(**
+This file is part of the coq-teach library
+
+Copyright (C) Boldo, Clément, Hamelin, Mayero, Rousselin
+
+This library is free software; you can redistribute it and/or
+modify it under the terms of the GNU Lesser General Public
+License as published by the Free Software Foundation; either
+version 3 of the License, or (at your option) any later version.
+
+This library is distributed in the hope that it will be useful,
+but WITHOUT ANY WARRANTY; without even the implied warranty of
+MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+COPYING file for more details.
+*)
+
+(** * Missing basic lemmas for the type [positive] of binary positive integers *)
+From Coq Require Import PArith.BinPos.
+
+Module Pos.
+Local Open Scope positive_scope.
+
+Lemma neq_1_lt_1 (p : positive) : p <> 1 <-> (1 < p).
+Proof.
+  split; [| now intros H H'; apply (Pos.lt_irrefl p); rewrite H' at 1].
+  destruct p as [p | p |]; [| | intros C; exfalso; apply C]; reflexivity.
+Qed.
+
+Lemma le_le_succ_r (n m : positive) :
+  n <= m -> n <= Pos.succ m.
+Proof.
+  intros H; apply Pos.le_trans with (1 := H).
+  apply Pos.lt_le_incl; exact (Pos.lt_succ_diag_r _).
+Qed.
+
+Lemma le_succ_r (n m : positive) :
+  (n <= Pos.succ m) <-> n <= m \/ n = Pos.succ m.
+Proof.
+  split.
+  - now intros [I%Pos.lt_succ_r | ->]%Pos.le_lteq; [left | right; reflexivity].
+  - intros [I | ->]; [apply le_le_succ_r; exact I | exact (Pos.le_refl _)].
+Qed.
+
+Lemma two_succ : 2 = Pos.succ 1.
+Proof. reflexivity. Qed.
+
+Lemma le_2_succ (n : positive) : 2 <= Pos.succ n.
+Proof. rewrite two_succ, <-Pos.succ_le_mono; exact (Pos.le_1_l _). Qed.
+End Pos.

addons/teach/workdir/theories/Pos_prime.v

+(**
+This file is part of the coq-teach library
+
+Copyright (C) Boldo, Clément, Hamelin, Mayero, Rousselin
+
+This library is free software; you can redistribute it and/or
+modify it under the terms of the GNU Lesser General Public
+License as published by the Free Software Foundation; either
+version 3 of the License, or (at your option) any later version.
+
+This library is distributed in the hope that it will be useful,
+but WITHOUT ANY WARRANTY; without even the implied warranty of
+MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+COPYING file for more details.
+*)
+From Coq Require Import ZArith.BinInt.
+From Teach Require Import Pos_Compl.
+Module Pos.
+Local Open Scope positive_scope.
+Definition primeb_pos_aux (p : positive) (fuel : positive) : bool.
+Proof.
+  induction fuel as [| fuel' IH'] using Pos.peano_rect.
+  - exact true.
+  - destruct (Z.pos p mod (Z.pos (Pos.succ fuel')) =? 0)%Z eqn:E.
+    + exact false.
+    + exact IH'.
+Defined.
+
+Lemma primeb_pos_aux_succ (p : positive) (fuel : positive) :
+  primeb_pos_aux p (Pos.succ fuel) =
+  if (Z.pos p mod (Z.pos (Pos.succ fuel)) =? 0)%Z then false else
+    primeb_pos_aux p fuel.
+Proof. 
+  unfold primeb_pos_aux;
+  rewrite Pos.peano_rect_succ;
+  destruct (Z.pos p mod (Z.pos (Pos.succ fuel)) =? 0)%Z eqn:E; reflexivity.
+Qed.
+
+Lemma primeb_pos_aux_correct (p : positive) (fuel : positive) :
+  primeb_pos_aux p fuel = true <->
+    forall (n : positive), (2 <= n <= fuel)%positive ->
+    (Z.pos p mod (Z.pos n) =? 0)%Z = false.
+Proof.
+  split; induction fuel as [| fuel' IH'] using Pos.peano_rect.
+  - intros _ n [C1 C2]; exfalso.
+    pose proof (Pos.le_trans _ _ _ C1 C2) as C.
+    unfold Pos.le in C; apply C; reflexivity.
+  - intros H n [In In'].
+    rewrite primeb_pos_aux_succ in H.
+    destruct (Z.pos p mod (Z.pos (Pos.succ fuel')) =? 0)%Z eqn:E; simpl in H.
+    + discriminate H.
+    + apply Pos.le_succ_r in In' as [In' | En].
+      * apply IH'; [exact H |]; split; assumption.
+      * rewrite En; exact E.
+  - intros _; reflexivity.
+  - intros H.
+    rewrite primeb_pos_aux_succ.
+    destruct (Z.pos p mod (Z.pos (Pos.succ fuel')) =? 0)%Z eqn:E; simpl.
+    + rewrite <-E; rewrite H; [reflexivity |]; split; [| exact (Pos.le_refl _)].
+      exact (Pos.le_2_succ _).
+    + apply IH'; intros n [In In']; apply H; split; [exact In |].
+      apply Pos.le_le_succ_r; exact In'. 
+Qed.
+End Pos.

addons/teach/workdir/theories/WS_Binomial.v

+(**
+This file is part of the coq-teach library
+
+Copyright (C) Boldo, Clément, Hamelin, Mayero, Rousselin
+
+This library is free software; you can redistribute it and/or
+modify it under the terms of the GNU Lesser General Public
+License as published by the Free Software Foundation; either
+version 3 of the License, or (at your option) any later version.
+
+This library is distributed in the hope that it will be useful,
+but WITHOUT ANY WARRANTY; without even the implied warranty of
+MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+COPYING file for more details.
+*)
+
+(** * Worksheet on binomial coefficients.
+
+ These are:
+ - general statements from library modules Nat_Sum, Nat_Factorial and
+   Nat_Binomial that are equipped with guidance comments for students, and
+   solution(s) for teachers;
+ - alternate proofs general results from the library modules;
+ - proofs that hypotheses of general results are optimal;
+ - or specific statements or questions.
+
+ Note that provided script prepsheet will replace lines from marker
+   (* Begin solution for the teacher. *)
+ to next marker (included)
+   (* End solution for the teacher. *)
+ by "Admitted.", and will remove lines from marker
+   (* Begin other solution for the teacher. *)
+ to next marker (included)
+   (* End other solution for the teacher. *)
+
+ That way, both teacher and student versions of the file are compiling, and
+ teachers can verify the validity of the provided solution(s). *)
+
+From Teach Require Import WS_Helper.
+
+Section Statements_From_Lib.
+Search "vandermonde".
+(*fr Faire la preuve du lemme suivant et remplacer "Admitted" par "Qed". *)
+(*en Fill the proof of next lemma and replace "Admitted" by "Qed". *)
+Lemma binom_sum_sqr n :
+  sum_range 0 n (fun k => (binom n k) ^ 2) = binom (2 * n) n.
+Proof.
+(*fr Transformer (2*n) en une somme. *)
+(*en Transform (2*n) into a sum. *)
+
+(*fr Utiliser l'identité de Vandermonde. *)
+(*en Use Vandermonde's identity. *)
+
+(*fr Réduire l'égalite de somme à l'égalité des fonctions. *)
+(*en Reduce equality on sums to equality on functions. *)
+
+(*fr Utiliser la symétrie des coefficients binomiaux. *)
+(*en Use symmetry of binomial coefficients. *)
+
+(*fr Ne pas oublier les conditions d'application des lemmes utilisés. *)
+(*en Do not forget application conditions of used lemmas. *)
+
+(* Begin solution for the teacher. *)
+(* Without automation. *)
+replace (2 * n) with (n + n) by apply double_twice.
+rewrite binom_vandermonde.
+apply sum_range_ext. intros k [_ Hk].
+rewrite <- binom_sym. 2: assumption.
+rewrite pow_2_r. reflexivity.
+Qed.
+(* End solution for the teacher. *)
+
+(* Begin other solution for the teacher. *)
+(* With automation. *)
+Lemma binom_sum_sqr_with_auto n :
+  sum_range 0 n (fun k => (binom n k) ^ 2) = binom (2 * n) n.
+Proof.
+replace (2 * n) with (n + n) by lia.
+rewrite binom_vandermonde.
+apply sum_range_ext. intros k Hk.
+rewrite <- binom_sym by lia.
+now rewrite pow_2_r.
+Qed.
+(* End other solution for the teacher. *)
+
+(*enFill the proof of next lemma and replace "Admitted" by "Qed". *)
+
+
+(*fr Faire la preuve du lemme suivant et remplacer "Admitted" par "Qed". *)
+(*enFill the proof of next lemma and replace "Admitted" by "Qed". *)
+Lemma binom_sum n : sum_range 0 n (fun k => binom n k) = 2 ^ n.
+Proof.
+(*fr Transformer 2 en une somme. *)
+(*en Transform 2 into a sum. *)
+
+(*fr Utiliser la formule du binome. *)
+(*en Use binomial theorem. *)
+
+(*fr Reduire l'egalite de somme a l'egalite des fonctions. *)
+(*en Reduce equality on sums to equality on functions. *)
+
+(* Begin solution for the teacher. *)
+(* Without automation. *)
+replace 2 with (1+1) by reflexivity.
+rewrite binom_formula.
+apply sum_range_ext. intros k Hk.
+rewrite !pow_1_l.
+rewrite !mul_1_r. reflexivity.
+Qed.
+(* End solution for the teacher. *)
+
+(* Begin other solution for the teacher. *)
+(* With automation. *)
+Lemma binom_sum_with_auto n : sum_range 0 n (fun k => binom n k) = 2 ^ n.
+Proof.
+replace 2 with (1+1) by easy.
+rewrite binom_formula.
+apply sum_range_ext. intros k Hk.
+rewrite !pow_1_l; lia.
+Qed.
+(* End other solution for the teacher. *)
+
+End Statements_From_Lib.
+
+
+Section Alternate_Proofs.
+
+(*fr Preuve alternative de la formule du pion. *)
+(*en Alternate proof of the committee-chair identity. *)
+Lemma binom_committee_chair_alt n k :
+  S k * binom n (S k) = n * binom (n - 1) k.
+Proof.
+  destruct n. now simpl.
+  destruct (le_lt_dec (S k) (S n)) as [h1|]. 2: rewrite 2!binom_eq_0; lia.
+  symmetry.
+  rewrite binom_fact_div_wn0 by lia.
+  replace (S n - 1) with n by lia.
+  rewrite <- divide_div_mul_exact.
+  * rewrite mul_comm, <- fact_S.
+    rewrite <- div_mul_cancel_l with (c := S k) by lia.
+    rewrite mul_assoc.
+    rewrite (mul_comm _ (fact k)), <- fact_S.
+    replace (n - k) with (S n - S k) by lia.
+    rewrite divide_div_mul_exact.
+    + now rewrite <- binom_fact_div_wn0.
+    + apply mod_divide.
+      apply fact_sub_mod_0; lia.
+  * apply mod_divide.
+    apply fact_sub_mod_0; lia.
+Qed.
+
+End Alternate_Proofs.
+
+
+Section Optimality_Of_Hypotheses.
+
+(*fr Prouver que les hypothèses des lemmes suivants sont optimales : *)
+(*en Prove that hypotheses of the following lemmas are optimal: *)
+(*   binom_S_l, binom_S_r, binom_pred, binom_eq_0, binom_gt_0, binom_neq_0,
+   binom_le_alt, binom_lt_S, binom_lt, binom_lt_alt, binom_gt_1,
+   binom_committee_chair_iter, binom_fact, binom_fact_div, binom_sym,
+   binom_cancellation_alt. *)
+
+(*fr Indication : ces lemmes sont de la forme (P -> Q). Il faut donc prouver
+ l'équivalence (P <-> Q), ou juste l'implication dans l'autre sens (Q -> P),
+ ou plutôt la contraposée de cette dernière (~ P -> ~ Q). *)
+(*en Hint: these lemmas are of the form (P -> Q). It is thus a matter of proving
+ either the equivalence (P <-> Q), or just the reverse implication (Q -> P),
+ or rather the contrapositive of the latter (~ P -> ~ Q). *)
+
+(* "_rev_contra" means the contrapositive of the reverse implication. *)
+
+Lemma binom_S_l_rev_contra n k :
+  k = 0 -> binom (S n) k <> binom n (pred k) + binom n k.
+Proof.
+intros; subst. simpl.
+rewrite !binom_0_r.
+apply lt_neq, lt_1_2.
+Qed.
+
+(*fr Ici, P est de la forme (~ P1 \/ ~ P2), sa négation est donc (P1 /\ P2). *)
+(*en Here, P is of the form (~ P1 \/ ~ P2), thus its negation is (P1 /\ P2). *)
+Lemma binom_S_r_rev_contra n k :
+  n = 0 /\ k = 0 -> binom n (S k) <> binom (pred n) k + binom (pred n) (S k).
+Proof.
+intros [Hn Hk]; subst. simpl.
+apply nat_neq_0_1.
+Qed.
+
+Lemma binom_pred_rev_contra n k :
+  n = 0 /\ k = 1 \/ k = 0 ->
+  binom n k <> binom (pred n) (pred k) + binom (pred n) k.
+Proof.
+intros [[Hn Hk] | Hk].
++ subst. simpl. apply nat_neq_0_1.
++ subst. rewrite !binom_0_r. apply not_eq_S, nat_neq_0_1.
+Qed.
+
+Lemma binom_eq_0_rev_contra n k : k <= n -> binom n k <> 0.
+Proof. apply binom_neq_0. Qed.
+
+Lemma binom_gt_0_rev_contra n k : n < k-> binom n k <= 0.
+Proof. rewrite le_0_r. apply binom_eq_0. Qed.
+
+Lemma binom_neq_0_rev_contra n k : n < k -> binom n k = 0.
+Proof. apply binom_eq_0. Qed.
+
+(*fr Ici, P est de la forme (P1 \/ P2 \/ P3), sa négation est donc
+ (~ P1 /\ ~ P2 /\ ~ P3). *)
+(*en Here, P is of the form (P1 \/ P2 \/ P3), thus its negation is
+ (~ P1 /\ ~ P2 /\ ~ P3). *)
+Lemma binom_le_alt_rev_contra n1 n2 k :
+  (k <> 0 /\ k <= n1 /\ n2 < n1) -> binom n2 k < binom n1 k.
+Proof.
+intros [Hk1 [Hk2 Hn]]. apply binom_lt. 2: assumption. split. 2: assumption.
+apply neq_0_lt_0. assumption.
+Qed.
+
+(*fr Ici, P est de la forme (P1 /\ P2), sa négation est donc (~ P1 \/ ~ P2). *)
+(*en Here, P is of the form (P1 /\ P2), thus its negation is (~ P1 \/ ~ P2). *)
+Lemma binom_lt_S_rev_contra n k :
+  (k <= 0 \/ S n < k) -> binom (S n) k <= binom n k.
+Proof.
+intros [Hk | H].
++ rewrite le_0_r in Hk. subst. simpl. rewrite binom_0_r. apply le_refl.
++ rewrite binom_eq_0. apply le_0_l. assumption.
+Qed.
+
+(*fr Ici, P est de la forme (P1 /\ P2 /\ P3), sa négation est donc
+ (~ P1 \/ ~ P2 \/ ~ P3). *)
+(*en Here, P is of the form (P1 /\ P2 /\ P3), thus its negation is
+ (~ P1 \/ ~ P2 \/ ~ P3). *)
+Lemma binom_lt_rev_contra n1 n2 k :
+  (k <= 0 \/ n2 < k \/ n2 <= n1) -> binom n2 k <= binom n1 k.
+Proof. rewrite le_0_r. apply binom_le_alt. Qed.
+
+(*fr Ici, P est de la forme (P1 /\ P2), sa négation est donc (~ P1 \/ ~ P2). *)
+(*en Here, P is of the form (P1 /\ P2), thus its negation is (~ P1 \/ ~ P2). *)
+Lemma binom_gt_1_rev_contra n k : k <= 0 \/ n <= k -> binom n k <= 1.
+Proof.
+rewrite le_0_r. intros [H | H].
++ subst. rewrite binom_0_r. apply le_refl.
++ destruct (le_lt_eq_dec _ _ H) as [H' | H'].
+  - rewrite binom_eq_0. apply le_0_l. assumption.
+  - subst. rewrite binom_diag. apply le_refl.
+Qed.
+
+(*fr Ici, P est de la forme (~ P1 \/ P2), sa négation est donc (P1 /\ ~ P2). *)
+(*en Here, P is of the form (~ P1 \/ P2), thus its negation is (P1 /\ ~ P2). *)
+Lemma binom_committee_chair_iter_rev_contra n k i :
+  (k = 0 /\ n < i) ->
+  fact (k + i) * fact (n - i) * binom n (k + i) <>
+    fact n * fact k * binom (n - i) k.
+Proof.
+intros [Hk H]; subst. simpl.
+rewrite binom_eq_0. 2: assumption.
+rewrite mul_0_r.
+rewrite nat_sub_0_lt. 2: assumption. simpl.
+rewrite !mul_1_r.
+apply not_eq_sym, fact_neq_0.
+Qed.
+
+Lemma binom_fact_rev_contra n k :
+  n < k -> binom n k * (fact k * fact (n - k)) <> fact n.
+Proof.
+intros H.
+rewrite binom_eq_0. 2: assumption. simpl.
+apply not_eq_sym, fact_neq_0.
+Qed.
+
+(*fr Ici, P est de la forme (~ P1 \/ ~ P2), sa négation est donc (P1 /\ P2). *)
+(*en Here, P is of the form (~ P1 \/ ~ P2), thus its negation is (P1 /\ P2). *)
+Lemma binom_fact_div_rev_contra n k :
+  (n = 0 /\ k = 1) -> binom n k <> fact n / (fact k * fact (n - k)).
+Proof. intros [Hn Hk]; subst. simpl. apply nat_neq_0_1. Qed.
+
+Lemma binom_sym_rev_contra n k : n < k ->  binom n k <> binom n (n - k).
+Proof.
+intros H.
+rewrite binom_eq_0. 2: assumption.
+rewrite nat_sub_0_lt. 2: assumption.
+rewrite binom_0_r.
+apply nat_neq_0_1.
+Qed.
+
+(*fr Ici, P est de la forme (P1 \/ P2), sa négation est donc (~ P1 /\ ~ P2). *)
+(*en Here, P is of the form (P1 \/ P2), thus its negation is (~ P1 /\ ~ P2). *)
+Lemma binom_cancellation_alt_rev_contra n k i :
+  k < i /\ i <= n ->
+  binom n k * binom k i <> binom n i * binom (n - i) (k - i).
+Proof.
+intros [H1 H2].
+rewrite (binom_eq_0 k i H1). rewrite mul_0_r.
+apply not_eq_sym, neq_mul_0. split; apply binom_neq_0.
++ assumption.
++ apply sub_le_mono_r.
+  apply lt_le_incl, lt_le_trans with i.
+  all: assumption.
+Qed.
+
+End Optimality_Of_Hypotheses.
+
+
+Section Specific_Statements.
+
+(*fr L'exercice suivant provient de *)
+(*en The following exercise is taken from *)
+(* Hyperbole Terminale - Spécialité Mathématiques, Nathan, 2020 (in French). *)
+
+(*fr Résoudre (binom n 5 = 17 (binom n 4)) avec (n >= 5).
+ Indication : essayer n = 89. *)
+(*en Solve (binom n 5 = 17 (binom n 4)) with (n >= 5).
+ Hint: try n = 89. *)
+
+Lemma binom_ex01a : exists n, 5 <= n /\ binom n 5 = 17 * binom n 4.
+Proof.
+exists 89. split.
++ apply sub_0_le. rewrite 5!sub_succ. apply sub_0_l.
++ apply (mul_cancel_l _ _ 5). discriminate.
+  rewrite binom_mul_S_r. rewrite 4!sub_succ, sub_0_r, mul_assoc. reflexivity.
+Qed.
+
+Lemma binom_ex01b n : binom n 5 = 17 * binom n 4 -> n < 5 \/ n = 89.
+Proof.
+destruct (nat_lt_le_dec n 5) as [Hn | Hn].
++ intros _; left. assumption.
++ assert (Hn' : 4 <= n).
+    apply le_trans with 5. apply le_succ_diag_r. assumption.
+  rewrite <- (mul_cancel_l _ _ 5). 2: discriminate.
+  rewrite binom_mul_S_r. rewrite mul_assoc. rewrite mul_cancel_r.
+  2: apply binom_neq_0; assumption.
+  intros H. apply nat_sub_add_eq_l in H. 2: assumption.
+  right. subst. reflexivity.
+Qed.
+
+End Specific_Statements.

addons/teach/workdir/theories/WS_Helper.v

+(**
+This file is part of the coq-teach library
+
+Copyright (C) Boldo, Clément, Hamelin, Mayero, Rousselin
+
+This library is free software; you can redistribute it and/or
+modify it under the terms of the GNU Lesser General Public
+License as published by the Free Software Foundation; either
+version 3 of the License, or (at your option) any later version.
+
+This library is distributed in the hope that it will be useful,
+but WITHOUT ANY WARRANTY; without even the implied warranty of
+MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+COPYING file for more details.
+ *)
+
+(** * Useful exports for the provided worksheet.
+ This includes the lists of results on natural numbers from Arith.PeanoNat.Nat
+ that are used in modules Nat_Sum, Nat_Factorial and Nat_Binomial.
+
+ Usage: tune exports and definitions to your needs, and import the resulting
+ module in the worksheet. *)
+
+From Coq Require Import Arith.PeanoNat.
+From Coq Require Export Arith.Compare_dec.
+From Coq Require Export Lia.
+
+Export (notations) Nat.
+
+(* Helper for results on natural numbers used in Nat_Sum. *)
+Export Nat (eq_add_0, eq_dec).
+Export Nat (le_0_l, le_refl, le_succ_diag_r, le_succ_l, le_trans, lt_pred_l,
+            lt_succ_diag_r, lt_succ_r, neq_0_lt_0, nle_gt, nlt_ge).
+Export Nat (add_0_l, add_0_r, add_1_r, add_assoc, add_comm, add_sub,
+            add_sub_assoc, add_sub_swap, add_succ_comm, add_succ_r, sub_0_r,
+            sub_1_r, sub_add, sub_add_distr, sub_diag, sub_succ, sub_succ_l).
+Export Nat (add_le_mono, le_add_l, le_add_r).
+Export Nat (mul_0_r, mul_add_distr_l, mul_comm).
+
+(* Helper for results on natural numbers used in Nat_Factorial. *)
+Export Nat (eq_dec, succ_pred).
+Export Nat (le_0_l, le_0_r, le_1_r, le_antisymm, le_lt_trans, le_refl,
+            le_succ_l, le_trans, nle_gt, nle_succ_0).
+Export Nat (lt_0_1, lt_0_succ, lt_le_trans, lt_neq, lt_succ_diag_r, lt_trans,
+            neq_0_lt_0, nlt_ge).
+Export Nat (add_0_r).
+Export Nat (mul_1_r, mul_assoc, mul_comm, mul_eq_0, mul_pos_pos, neq_mul_0).
+Export Nat (div_mul, divide_factor_r, divide_mul_l, mod_divides).
+
+(* Helper for results on natural numbers used in Nat_Binomial. *)
+Export Nat (eq_dec, pred_succ, succ_pred).
+Export Nat (le_0_l, le_0_r, le_antisymm, le_refl, le_trans, le_succ_diag_r,
+            le_succ_le_pred, le_trans).
+Export Nat (lt_0_1, lt_0_succ, lt_1_r, lt_le_incl, lt_neq, lt_succ_diag_r,
+            lt_succ_lt_pred, lt_succ_r, lt_trans, neq_0_lt_0, nle_gt, nlt_ge,
+            succ_le_mono, succ_lt_mono).
+Export Nat (add_0_l, add_0_r, add_1_l, add_1_r, add_assoc, add_comm, add_sub,
+            add_sub_swap, add_succ_comm, add_succ_r, sub_0_l, sub_0_le,
+            sub_0_r, sub_1_r, sub_add, sub_diag, sub_succ_l, sub_succ_r).
+Export Nat (add_lt_mono_r, add_pos_l, le_add_l, lt_add_pos_l, lt_lt_add_l).
+Export Nat (mul_0_l, mul_0_r, mul_1_l, mul_1_r, mul_assoc, mul_cancel_l,
+            mul_comm, mul_succ_l).
+Export Nat (double_twice, mul_add_distr_l, mul_add_distr_r).
+Export Nat (div_mul, div_small, mod_divides).
+Export Nat (pow_0_r, pow_1_l, pow_2_r, pow_succ_r').
+
+(* Helper for results on natural numbers used in exercises. *)
+Export Nat (lt_1_2).
+Export Nat (add_sub_eq_l, add_succ_l, sub_le_mono_r).
+Export Nat (mul_cancel_r, mul_le_mono_l, mul_le_mono_pos_r, mul_sub_distr_r).
+Export Nat (div_mul_cancel_l, div_unique_exact, divide_div_mul_exact,
+            mod_divide).
+Export Nat (pow_inj_l, pow_le_mono_l, pow_mul_l).
+
+From Teach Require Export Nat_Compl Nat_Sum Nat_Factorial.
+From Teach Require Import Nat_Binomial.
+Export Nat_Binomial (binom, binom_vandermonde, binom_sym, binom_formula, binom_eq_0, binom_fact_div_wn0,
+                     fact_sub_mod_0, binom_0_r, binom_neq_0, binom_lt, binom_le_alt, binom_diag, binom_mul_S_r).
+Export Nat_Compl.Nat.
+
+Definition formule_du_pion := binom_committee_chair.
+Definition committee_chair_identity := binom_committee_chair.
+Definition formule_de_vandermonde := binom_vandermonde.
+Definition vandermonde_identity := binom_vandermonde.
+

addons/teach/workdir/theories/Zmod_div.v

+(**
+This file is part of the coq-teach library
+
+Copyright (C) Boldo, Clément, Hamelin, Mayero, Rousselin
+
+This library is free software; you can redistribute it and/or
+modify it under the terms of the GNU Lesser General Public
+License as published by the Free Software Foundation; either
+version 3 of the License, or (at your option) any later version.
+
+This library is distributed in the hope that it will be useful,
+but WITHOUT ANY WARRANTY; without even the implied warranty of
+MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+COPYING file for more details.
+*)
+
+From Coq.ZArith Require Import BinInt Wf_Z.
+
+(** ** Missing lemmas about modular arithmetics in Z *)
+
+Module Z.
+#[local] Open Scope Z.
+(** Below are lemmas either missing, or with unnecessary hypotheses, or wrong
+name in the standard library. *)
+
+Lemma div_eucl_0_r (a : Z) : Z.div_eucl a 0 = (0, a).
+Proof. destruct a as [| a | a]; reflexivity. Qed.
+
+Lemma div_eucl_0_l (b : Z) : Z.div_eucl 0 b = (0, 0).
+Proof. reflexivity. Qed.
+
+(* Alternative: Zdiv.Zmod_0_r *)
+Lemma mod_0_r (a : Z) : a mod 0 = a.
+Proof.
+  pose proof (div_eucl_0_r a) as E.
+  unfold "mod"; rewrite E; reflexivity.
+Qed.
+
+(* Alternative: Zdiv.Zdiv_0_r *)
+Lemma div_0_r (a : Z) : a / 0 = 0.
+Proof.
+  pose proof (div_eucl_0_r a) as E.
+  unfold "/"; rewrite E; reflexivity.
+Qed.
+
+(* Alternative: Zdiv.Zmod_0_l, better than Z.mod_0_l *)
+Lemma mod_0_l (b : Z) : 0 mod b = 0.
+Proof.
+  pose proof (div_eucl_0_l b) as E.
+  unfold "mod"; rewrite E; reflexivity.
+Qed.
+
+(* Alternative: Zdiv.Zdiv_0_l, better than Z.div_0_l *)
+Lemma div_0_l (b : Z) : 0 / b = 0.
+Proof.
+  pose proof (div_eucl_0_l b) as E.
+  unfold "/"; rewrite E; reflexivity.
+Qed.
+
+(* Better version of Z.div_mod *)
+Lemma div_mod (a b : Z) : a = b * (a / b) + a mod b.
+Proof.
+  destruct (Z.eq_dec b 0) as [-> | E].
+  - rewrite div_0_r, mod_0_r; reflexivity.
+  - exact (Z.div_mod a b E).
+Qed.
+
+(* Better version of Z.mod_mul, better name than Zdiv.Z_mod_mult
+    Note that (a * b) / b = a is not valid in general if b = 0. *)
+Lemma mod_mul (a b : Z) : (a * b) mod b = 0.
+Proof.
+  pose proof (div_mod (a * b) b) as eq.
+  destruct (Z.eq_dec b 0) as [-> | Eb].
+  - rewrite mod_0_r, Z.mul_0_r; reflexivity.
+  - rewrite Z.div_mul, (Z.mul_comm b a) in eq by (exact Eb).
+    rewrite <-(Z.add_0_r (a * b)) in eq at 1.
+    apply Z.add_reg_l in eq; symmetry; exact eq.
+Qed.
+
+(* Better version of Znumtheory.Zmod_divide and Z.mod_divide, both have
+   the extra hypothesis [(b <> 0)], Z.mod_divide is an equivalence. *)
+Lemma mod_divide (a b : Z) : a mod b = 0 <-> (b | a).
+Proof.
+  pose proof (div_mod a b) as eq; split.
+  - intros H; rewrite H, Z.add_0_r, Z.mul_comm in eq; exists (a / b); exact eq.
+  - intros [q ->]; exact (mod_mul _ _).
+Qed.
+
+(* Better version of Z.add_mod *)
+Lemma add_mod (a b n : Z) : (a + b) mod n = (a mod n + b mod n) mod n.
+Proof.
+  destruct (Z.eq_dec n 0) as [-> | H].
+  - rewrite !mod_0_r; reflexivity.
+  - exact (Z.add_mod a b n H).
+Qed.
+
+(* NOTE: Z.mul_mod but without the unnecessary hypothesis *)
+Lemma mul_mod (a b n : Z) : (a * b) mod n = (a mod n * (b mod n)) mod n.
+Proof.
+  destruct (Z.eq_dec n 0) as [-> | H]; [now rewrite !Z.mod_0_r |].
+  exact (Z.mul_mod a b n H).
+Qed.
+
+(* NOTE: Z.mul_mod_idemp_r but without the unnecessary hypothesis *)
+Lemma mul_mod_idemp_r (a b n : Z) : (a * (b mod n)) mod n = (a * b) mod n.
+Proof.
+  destruct (Z.eq_dec n 0) as [-> | H].
+  - rewrite !Z.mod_0_r; reflexivity.
+  - rewrite Z.mul_mod_idemp_r by (exact H); reflexivity.
+Qed.
+
+(* Currently not in the stdlib *)
+Lemma pow_mod (a k n : Z) : (a ^ k) mod n = ((a mod n) ^ k) mod n.
+Proof.
+  destruct (Z.neg_nonneg_cases k).
+  - rewrite 2Z.pow_neg_r by (assumption); reflexivity.  (* <- ugly *)
+  - apply (Wf_Z.natlike_ind (fun k => a ^ k mod n = (a mod n) ^ k mod n)); (* <- ugly *)
+      [rewrite 2Z.pow_0_r; reflexivity | | exact H].
+    intros x Hx IH; rewrite 2Z.pow_succ_r, mul_mod, IH by (assumption).
+    rewrite mul_mod_idemp_r; reflexivity.
+Qed.
+
+(* Currently does not exist in the stdlib, note the unfortunate condition *)
+Lemma pow_m1_l_odd (n : Z) : (0 <= n) -> Z.Odd n -> (- 1) ^ n = - 1.
+Proof.
+  intros H H'.
+  replace (- 1) with (- (1)) by reflexivity. (* <- ugly *)
+  rewrite Z.pow_opp_odd by (exact H').
+  rewrite Z.pow_1_l by exact H; reflexivity.
+Qed.
+
+Lemma gcd_ge_1 (a b : Z) : a <> 0 \/ b <> 0 -> 1 <= Z.gcd a b.
+Proof.
+  intros Hab; rewrite Z.one_succ; apply Z.le_succ_l, Z.le_neq; split.
+  - exact (Z.gcd_nonneg _ _).
+  - intros [Ha Hb]%eq_sym%Z.gcd_eq_0; destruct Hab as [Ha' | Hb'];
+      [exact (Ha' Ha) | exact (Hb' Hb)].
+Qed.
+
+Lemma gt_1_neq_0 (n : Z) : 1 < n -> n <> 0.
+Proof.
+  intros H1 H2; apply (Z.lt_asymm 1 n); [exact H1 | rewrite H2; exact Z.lt_0_1].
+Qed.
+
+Lemma ge_1_gt_0 (n : Z) : 1 <= n -> 0 < n.
+Proof. rewrite Z.one_succ; intros H%Z.le_succ_l; exact H. Qed.
+
+Lemma gt_1_gt_0 (n : Z) : 1 < n -> 0 < n.
+Proof. intros H; apply Z.lt_trans with (1 := Z.lt_0_1); exact H. Qed.
+
+(* Equivalence in Z.divide_add_cancel_r *)
+(* NOTE: the stdlib is inconsistent in the naming of "cancel_l" or "cancel_r"
+lemmas, most of the times "l" or "r" refers to the position of the canceled
+operand, but sometimes (see [Z.divide_add_cancel_r]) it refers to the position
+of the uncanceled operand.
+See also the ouput of [Search "cancel_r"].
+We chose "l" or "r" to denote the position of the canceled operand as we believe
+it's probably what the user expects. *)
+
+Lemma divide_add_cancel_l (n m p : Z) : (n | m) -> (n | m + p) <-> (n | p).
+Proof.
+  intros H; split.
+  - exact (Z.divide_add_cancel_r _ _ _ H).
+  - exact (Z.divide_add_r _ _ _ H).
+Qed.
+
+Lemma divide_add_cancel_r (n m p : Z) : (n | m) -> (n | p + m) <-> (n | p).
+Proof. rewrite Z.add_comm; exact (divide_add_cancel_l _ _ _). Qed.
+
+(* Equivalence in Gauss lemma *)
+Lemma divide_mul_cancel_l (n m p : Z) :
+  Z.gcd n m = 1 -> (n | m * p) <-> (n | p).
+Proof.
+  intros H; split.
+  - intros H'; exact (Z.gauss _ _ _ H' H).
+  - clear H; exact (Z.divide_mul_r _ _ _).
+Qed.
+
+Lemma divide_mul_cancel_r (n m p : Z) :
+  Z.gcd n m = 1 -> (n | p * m) <-> (n | p).
+Proof. rewrite Z.mul_comm; exact (divide_mul_cancel_l _ _ _). Qed.
+
+End Z.

addons/teach/workdir/theories/Zprime.v

+(**
+This file is part of the coq-teach library
+
+Copyright (C) Boldo, Clément, Hamelin, Mayero, Rousselin
+
+This library is free software; you can redistribute it and/or
+modify it under the terms of the GNU Lesser General Public
+License as published by the Free Software Foundation; either
+version 3 of the License, or (at your option) any later version.
+
+This library is distributed in the hope that it will be useful,
+but WITHOUT ANY WARRANTY; without even the implied warranty of
+MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+COPYING file for more details.
+*)
+
+From Coq Require Import ZArith.BinInt Znumtheory.
+From Teach Require Import Zmod_div Pos_prime Pos_Compl.
+
+(** * Additional lemmas and functions about primality in Z *)
+
+(** Remark: the definition of the [prime] predicate (Prop-valued) is in 
+   ZArith.Znumtheory. It is quite surprising and not very practical. *)
+
+Module Z.
+(* Alternative (better) definitions of prime *)
+Lemma prime_no_strict_divisor (p : Z) :
+  prime p <-> 1 < p /\ forall a, (a | p) -> a = -1 \/ a = 1 \/ a = p \/ a = - p.
+Proof.
+  split; intros H.
+  - pose proof H as [H1 H2]; split; [exact H1 |].
+    exact (Znumtheory.prime_divisors p H).
+  - destruct H as [H1 H2]; constructor; [exact H1 |].
+    intros n Hn; apply Znumtheory.Zgcd_1_rel_prime.
+    apply Z.le_antisymm; cycle 1;
+      [apply Z.gcd_ge_1; right; apply Z.gt_1_neq_0; exact H1 |].
+    apply Z.le_ngt; intros H.
+    pose proof (Z.gcd_divide_r n p) as Hdiv.
+    pose proof (Z.gcd_nonneg n p) as Ig.
+    pose proof (Z.gcd_divide_l n p) as Hdivn.
+    specialize (H2 _ Hdiv) as [C | [C | [C | C]]].
+    + rewrite C in Ig; apply Z.le_ngt in Ig; now apply Ig.
+    + rewrite C in H; apply (Z.lt_irrefl 1); exact H.
+    + rewrite C in Hdivn.
+      apply Z.divide_pos_le, Z.le_ngt in Hdivn; [| now apply Z.ge_1_gt_0, Hn].
+      now apply Hdivn, Hn.
+    + rewrite C in Ig; apply Z.le_ngt in Ig.
+      apply Ig, Z.opp_neg_pos, Z.gt_1_gt_0; exact H1.
+Qed.
+
+Lemma prime_no_strict_divisor_below (p : Z) :
+  prime p <-> 1 < p /\ forall a, 1 < a < p -> ~ (a | p).
+Proof.
+  split.
+  - intros H; pose proof H as [H1 H2]; split; [exact H1 |]; intros a Ha Hdiv.
+    apply prime_no_strict_divisor in H as [_ H].
+    specialize (H a Hdiv) as [C | [C | [C | C]]]; rewrite C in Ha.
+    + destruct Ha as [Ha _]; now apply (Z.lt_asymm (-1) 1).
+    + destruct Ha as [Ha _]; apply (Z.lt_irrefl 1); exact Ha.
+    + destruct Ha as [_ Ha]; apply (Z.lt_irrefl p); exact Ha.
+    + destruct Ha as [Ha _]; apply (Z.lt_asymm (- p) 1); [| exact Ha].
+      now apply Z.lt_trans with (2 := Z.lt_0_1), Z.opp_neg_pos, Z.gt_1_gt_0.
+  - intros [Ip Hp]; apply prime_no_strict_divisor; split; [exact Ip |].
+    intros a Hdiv; enough (Z.abs a = 1 \/ Z.abs a = p) as C. {
+      destruct C as [C | C].
+      + destruct (Z.abs_or_opp_abs a) as [C' | C']; [right; left | left];
+          rewrite C'; [exact C |]; rewrite C; exact (Pos2Z.opp_pos _).
+      + right; right; destruct (Z.abs_or_opp_abs a) as [C' | C'];
+          [left | right]; rewrite C', C; reflexivity.
+    }
+    apply Z.divide_abs_l in Hdiv.
+    pose proof (Z.abs_nonneg a) as [I1 | E1]%Z.le_lteq; cycle 1. {
+      exfalso; rewrite <-E1 in Hdiv; apply Z.divide_0_l in Hdiv;
+      rewrite Hdiv in Ip; apply (Z.lt_asymm 0 1 (Z.lt_0_1)); exact Ip.
+    }
+    pose proof (Z.gt_1_gt_0 p Ip) as Hpgt0.
+    pose proof (Z.divide_pos_le (Z.abs a) p Hpgt0 Hdiv) as I2.
+    assert (Z.abs a = 1 \/ 1 < Z.abs a) as [Ha | Ha]. {
+      apply Z.le_succ_l in I1; rewrite <-Z.one_succ in I1.
+      apply Z.le_lteq in I1 as [H | H]; [right | left; symmetry]; exact H.
+    }
+    + left; exact Ha.
+    + apply Z.le_lteq in I2 as [I2 | E2]; [| right; exact E2].
+      exfalso; apply (Hp (Z.abs a)); [| exact Hdiv]; split; assumption.
+Qed.
+
+Lemma divisor_le_sqrt (n m p : Z) :
+  0 <= n -> n = m * p -> m <= Z.sqrt n \/ p <= Z.sqrt n.
+Proof.
+  intros H1 Hdiv.
+  destruct (Z.le_ge_cases m 0) as [Im | Im]. {
+    left; apply Z.le_trans with (1 := Im); exact (Z.sqrt_nonneg _).
+  }
+  destruct (Z.le_ge_cases p 0) as [Ip | Ip]. {
+    right; apply Z.le_trans with (1 := Ip); exact (Z.sqrt_nonneg _).
+  }
+  destruct (Z.le_ge_cases m p) as [Imp | Imp]; [left | right].
+  - apply Z.sqrt_le_square; [exact H1 | exact Im |].
+    apply Z.mul_le_mono_nonneg_l with (1 := Im) in Imp; rewrite <-Hdiv in Imp;
+    exact Imp.
+  - apply Z.sqrt_le_square; [exact H1 | exact Ip |].
+    apply Z.mul_le_mono_nonneg_r with (1 := Ip) in Imp; rewrite <-Hdiv in Imp;
+    exact Imp.
+Qed.
+
+Lemma prime_no_strict_divisor_below_sqrt (p : Z) :
+  prime p <-> 1 < p /\ forall a, 1 < a <= Z.sqrt p -> ~ (a | p).
+Proof.
+  split.
+  - intros [Ip Hp]%prime_no_strict_divisor_below; split; [exact Ip |].
+    intros a [Ia Ia']; apply Hp; split; [exact Ia |].
+    apply Z.le_lt_trans with (1 := Ia').
+    apply Z.sqrt_lt_lin; exact Ip.
+  - intros [Ip Hp]; apply prime_no_strict_divisor_below; split; [exact Ip |].
+    intros a [Ia Ia'] [q Hq].
+    pose proof Hq as Hdiv; apply divisor_le_sqrt in Hdiv; cycle 1. {
+      apply Z.lt_le_incl, Z.gt_1_gt_0; exact Ip.
+    }
+    destruct Hdiv as [Hdiv | Hdiv].
+    + assert (1 < q) as Iq. {
+        apply Z.lt_nge; intros C.
+        apply (Z.mul_le_mono_nonneg_r _ _ a) in C; cycle 1. {
+          apply Z.lt_le_incl, Z.lt_trans with (1 := Z.lt_0_1); exact Ia.
+        }
+        rewrite <-Hq, Z.mul_1_l in C; apply Z.le_ngt in C; apply C; exact Ia'.
+      }
+      pose proof (conj Iq Hdiv) as Iq'; specialize (Hp _ Iq'); apply Hp.
+      exists a; rewrite Z.mul_comm; exact Hq.
+    + pose proof (conj Ia Hdiv) as Ia''; specialize (Hp _ Ia''); apply Hp.
+      exists q; exact Hq.
+Qed.
+
+Definition primeb (n : Z) : bool :=
+  match n with
+  | Z.neg p => false
+  | 0 => false
+  | Z.pos p =>
+    match p with
+    | 1%positive => false
+    | _ => Pos.primeb_pos_aux p (Z.to_pos (Z.sqrt (Z.pos p)))
+    end
+  end.
+
+Lemma Private_test_primeb :
+  primeb (- 5)  = false /\
+  primeb (- 4)  = false /\
+  primeb (- 3)  = false /\
+  primeb (- 2)  = false /\
+  primeb (- 1)  = false /\
+  primeb 0      = false /\
+  primeb 1      = false /\
+  primeb 2      = true  /\
+  primeb 3      = true  /\
+  primeb 4      = false /\
+  primeb 5      = true  /\
+  primeb 6      = false /\
+  primeb 7      = true  /\
+  primeb 8      = false /\
+  primeb 9      = false /\
+  primeb 10     = false /\
+  primeb 11     = true  /\
+  primeb 12     = false /\
+  primeb 13     = true  /\
+  primeb 14     = false /\
+  primeb 15     = false /\
+  primeb 16     = false /\
+  primeb 17     = true  /\
+  primeb 18     = false /\
+  primeb 19     = true  /\
+  primeb 65537  = true  /\
+  primeb 65533  = false /\
+  primeb 939391 = true. (* /\
+  primeb 479001599 = true. *)
+Proof. repeat split; reflexivity. Qed.
+
+Lemma primeb_correct (n : Z) : primeb n = true <-> prime n.
+Proof.
+  unfold primeb; split; destruct n as [| p | p].
+  - intros H; discriminate H. 
+  - enough (forall p, (p <> 1)%positive ->
+      Pos.primeb_pos_aux p (Z.to_pos (Z.sqrt (Z.pos p))) = true ->
+      prime (Z.pos p)) as key. {
+      destruct p as [p' | p' |]; [| | intros H; discriminate H]; apply key;
+        unfold Pos.le; intros H; discriminate H.
+    }
+    intros q Hq.
+    intros H; rewrite Pos.primeb_pos_aux_correct in H. (* apply fails *)
+    apply Z.prime_no_strict_divisor_below_sqrt; split. {
+      apply Pos2Z.pos_lt_pos, Pos.neq_1_lt_1; exact Hq.
+    }
+    intros a [Ha Ha']; intros Hdiv%Z.mod_divide%Z.eqb_eq.
+    destruct a as [| a | a]; [discriminate Ha | | discriminate Ha].
+    lapply (H a); [rewrite Hdiv; intros contra; discriminate contra |].
+    split.
+    + rewrite Pos.two_succ; apply Pos.le_succ_l; exact Ha.
+    + exact Ha'.
+  - intros H; discriminate H.
+  - intros [H _]; easy.
+  - enough (forall p, (p <> 1)%positive -> prime (Z.pos p) ->
+      Pos.primeb_pos_aux p (Z.to_pos (Z.sqrt (Z.pos p))) = true) as key. {
+      now intros Hp; destruct p as [p | p |];
+        [apply key.. | apply not_prime_1 in Hp].
+    }
+    intros q Hq Pq; apply Pos.primeb_pos_aux_correct; intros n Hn.
+    apply Z.prime_no_strict_divisor_below_sqrt in Pq as [_  Pq].
+    apply Z.eqb_neq; intros Hdiv%Z.mod_divide.
+    specialize (Pq (Z.pos n)); apply Pq; [| exact Hdiv].
+    destruct Hn as [H2%Pos2Z.pos_le_pos Hsqrt%Pos2Z.pos_le_pos].
+    split.
+    * apply Z.le_succ_l; rewrite <-Z.two_succ; exact H2.
+    * rewrite Z2Pos.id in Hsqrt; [exact Hsqrt | now apply Z.sqrt_pos].
+  - now intros [I _]; contradict I.
+Qed.
+End Z.