Require Import ssreflect.

Check 5.

Check 5+5.

Eval compute in 5×5.

Set Printing All.
Check 5.
Unset Printing All.

Definition pred n :=
  match n with
    | 0 ⇒ 0
    | S n ⇒ n
  end.

Eval compute in pred 5.

Fixpoint plus n m :=
  match n with
    | 0 ⇒ m
    | S n ⇒ S (plus n m)
  end.

Eval compute in plus 5 5.

Infix "+" := plus: nat_scope.

Check 5+5.

Lemma plus_0n: ∀ n, 0+n = n.
Proof.
  intro n.
  simpl.
  reflexivity.

  Restart.
  now destruct n.
Qed.

Lemma plus_n0: ∀ n, n+0 = n.
Proof.
  induction n.
   reflexivity.
   simpl. rewrite IHn. reflexivity.

  Restart.
  induction n; cbn; congruence.
Qed.

Lemma plus_assoc: ∀ n m p, n+(m+p) = (n+m)+p.
Proof.
  intros n m p.
  induction n.
   reflexivity.
   simpl. now rewrite IHn.

  Restart.
  induction n; cbn; congruence.
Qed.

Lemma plus_nS: ∀ n m, n+(S m) = S (n+m).
Proof.
  intros n m.
  induction n.
   reflexivity.
   simpl. now rewrite IHn.

  Restart.
  induction n; cbn; congruence.
Qed.

Lemma plus_comm: ∀ n m, n+m = m+n.
Proof.
  intros n m.
  induction n; simpl.
  - rewrite plus_n0. reflexivity.
  - rewrite plus_nS IHn. reflexivity.

  Restart.
  induction n; cbn; trivial.
  intros. now rewrite plus_nS IHn.
Qed.

Fixpoint mult n m :=
  match n with
    | 0 ⇒ 0
    | S n ⇒ m + mult n m
  end.

Infix "×" := mult: nat_scope.

Lemma mult_n0: ∀ n, n×0 = 0.
Proof.
  now induction n.
Qed.

Lemma mult_nS: ∀ n m, n*(S m) = n+n×m.
Proof.
  intros n m.
  induction n.
   reflexivity.
   simpl. rewrite IHn. now rewrite 2!plus_assoc (plus_comm m).
Qed.

Lemma mult_comm: ∀ n m, n×m = m×n.
Proof.
  intros n m.
  induction n; simpl.
  - now rewrite mult_n0.
  - now rewrite mult_nS IHn.
Qed.

Lemma mult_distr_plus_l: ∀ n m p, (n+m)*p = n×p+m×p.
Proof.
  intros n m p.
  induction n.
  - reflexivity.
  - simpl. rewrite IHn. apply plus_assoc.
Qed.

Lemma mult_assoc: ∀ n m p, n*(m×p) = (n×m)*p.
Proof.
  intros n m p.
  induction n.
   reflexivity.
   simpl. now rewrite IHn mult_distr_plus_l.
Qed.

Lemma mult_distr_plus_r: ∀ n m p, p*(n+m) = p×n+p×m.
Proof.
  intros n m p. now rewrite mult_comm mult_distr_plus_l 2!(mult_comm p).
Qed.

Lemma remarquable: ∀ n m, (n+m)*(n+m) = n×n + 2×n×m + m×m.
Proof.
  intros n m.
  rewrite mult_distr_plus_r 2!mult_distr_plus_l.
  rewrite (mult_comm m)/=.
  rewrite 2!mult_distr_plus_l/=.
  rewrite plus_n0/=.
  rewrite 2!plus_assoc//.
Qed.

Require Import Arith Psatz.
Import Nat.


Goal ∀ n m, (n+m)*(n+m) = n×n+2*n×m+m×m.
Proof.
  intros. ring.
  Restart.
  intros. ring_simplify. reflexivity.
Qed.

Goal ∀ n m, n×n = m → (n+m)*(n+m) = (2*n+1+m)*m.
Proof.
  intros n m H.
  rewrite -H. ring.
Qed.

Goal ∀ n m p, n < m ≤ p → 2*p-m < 2*p-n.
Proof. intros. lia. Qed.

Goal ∀ n m p, n < m ≤ p → ~(p<n).
Proof. intros. lia. Qed.

Goal ∀ n m, n ≤ m → m - (m - n) = n.
Proof. intros. lia. Qed.

Goal ∀ n m, m - (m - n) = n ∨ m < n.
Proof. intros. lia. Qed.

Fixpoint fact n :=
  match n with
  | 0 ⇒ 1
  | S n' ⇒ fact n' × n
  end.

Lemma fact_neq0: ∀ n, fact n ≠ 0.
Proof. induction n; cbn; lia. Qed.

Fixpoint C n k :=
  match n,k with
  | _,0 ⇒ 1
  | 0,_ ⇒ 0
  | S n',S k' ⇒ C n' k' + C n' k
  end.

Lemma Cn0: ∀ n, C n 0 = 1.
Proof. now destruct n. Qed.

Lemma Cn1: ∀ n, C n 1 = n.
Proof.
  induction n; cbn; trivial.
  now rewrite Cn0 IHn.
Qed.

Lemma Cn2: ∀ n, C n 2 × 2 = n × (n - 1).
Proof.
  induction n; cbn; trivial.
  rewrite Cn1.
  transitivity (n×2 + C n 2 × 2). ring.
  rewrite IHn. destruct n; cbn; lia.
Qed.

Lemma Czer: ∀ n k, n<k → C n k = 0.
Proof.
  induction n; cbn; intros [|k] nk; try lia.
  rewrite IHn. lia.
  rewrite IHn. lia.
  reflexivity.
Qed.

Lemma Cnn: ∀ n, C n n = 1.
Proof.
  induction n; cbn.
  - reflexivity.
  - rewrite IHn Czer; lia.
Qed.

Lemma factC: ∀ n k, k≤n → fact n = C n k × fact k × fact (n - k).
Proof.
  induction n; intros [|k] H; cbn; try lia.
  destruct (eq_nat_dec k n) as [<-|H'].
  - rewrite Cnn. rewrite Czer. lia.
    rewrite sub_diag. cbn. lia.
  - transitivity ( C n k × fact k × fact (n-k) × S k
                   + C n (S k) × fact (S k) × fact (n-S k) × (n - k)
                 ).
    rewrite -!IHn; lia.
    set c := C n k.
    set d := C n (S k).
    replace (n-k) with (S (n-S k)) by lia.
    cbn. ring.
Qed.

Corollary Cfact: ∀ n k, k≤n → C n k = fact n / (fact k × fact (n - k)).
Proof.
  intros. rewrite (factC n k)//.
  rewrite -mul_assoc div_mul//.
  by rewrite -neq_mul_0; split; apply fact_neq0.
Qed.

Lemma Csym: ∀ n k, k ≤ n → C n k = C n (n - k).
Proof.
  intros n k H.
  apply mul_cancel_l with (fact k × fact (n - k)).
  by rewrite -neq_mul_0; split; apply fact_neq0.
  transitivity (fact n).
  - rewrite (factC n k); lia.
  - rewrite (factC n (n-k)). lia.
    replace (n-(n-k)) with k; lia.
Qed.

Lemma Cpion: ∀ n k, C (S n) (S k) × S k = C n k × S n.
Proof.
  intros n k. destruct (le_lt_dec k n) as [L|L].
  - apply mul_cancel_l with (fact k × fact (n - k)).
    by rewrite -neq_mul_0; split; apply fact_neq0.
    transitivity (fact (S n)).
    -- rewrite (factC (S n) (S k)). lia.
       simpl. lia.
    -- cbn. rewrite (factC n k); lia.
  - rewrite !Czer; lia.
Qed.

Lemma nat_ind_2 (P: nat → Prop):
  P 0 → P 1 → (∀ n, P n → P (2+n)) → ∀ n, P n.
Proof.
  intros H0 H1 HSS.
  assert (G: ∀ m, P m ∧ P (S m)).
   induction m. split; assumption.
   split. apply IHm. apply HSS, IHm.
  apply G.
Qed.

Require Import Peano_dec Lt.
Check eq_nat_dec. Search lt.
Lemma nat_ind_lt (P: nat → Prop):
  (∀ n, (∀ m, m<n → P m) → P n) → ∀ n, P n.
Proof.
  intros HP.
  assert (G: ∀ n m, m<n → P m).
   induction n; intros m Hm.
    lia.
    case (eq_nat_dec m n).
     intros →. apply HP, IHn.
     intro D. apply IHn. lia.
  intro n. apply (G (S n) n). lia.

  Restart.
  intros HP.
  assert (G: ∀ n m, m<n → P m).
   induction n; intros m Hm.
    inversion Hm.
    case (eq_nat_dec m n).
     intros →. apply HP, IHn.
     intro D. apply IHn. apply lt_gt_cases in D as [D|D]. assumption.
     rewrite lt_succ_r in Hm. apply (le_lt_trans _ _ _ Hm) in D.
     destruct (lt_irrefl _ D).
  intro n. apply (G (S n) n). apply lt_succ_diag_r.
Qed.