(***************************************************************)
(* From Coq Require Import BinInt Zify. *)
Local Set Warnings "-notation-overridden".
Local Set Warnings "-ambiguous-paths".
From mathcomp Require Import all_ssreflect all_fingroup all_algebra.
From HB Require Import structures.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Open Scope ring_scope.

Import GRing.Theory.

Section sandbox.
Variable K : numFieldType.

Lemma sum_n_ssr_test2 n :
  \sum_(0 <= i < n) (i%:R) = n%:R * (n%:R - 1) / 2 :> K.
Proof.
elim: n => [ // | p Ih].
  rewrite big_geq.
    rewrite !mul0r.
    by [].
  by [].
rewrite -natr1.
rewrite addrK.
rewrite -(mulrC p%:R).
rewrite (_ : p%:R + 1 = p%:R - 1 + 2); last first.
  rewrite (_ : 2 = 1 + 1); last by [].
  rewrite addrA.
  rewrite subrK.
  by [].
rewrite -mulrA.
rewrite mulrDl.
have twon0 : 2 != 0 :> K by rewrite mulrz_neq0 oner_neq0.
rewrite (mulfV twon0).
rewrite mulrDr.
rewrite mulr1.
rewrite mulrA.
rewrite -Ih.
rewrite big_nat_recr.
rewrite /=.
  by [].
by [].
Qed.

Definition rotmx n : 'M[K]_n :=
  \matrix_(i < n, j < n) (((i.+1 %% n) == j)%N)%:R.

Lemma rotmx_det_2 : \det (rotmx 2) = -1.
Proof.
rewrite /rotmx.
rewrite (expand_det_col _ 0).
rewrite big_ord_recr.
rewrite /=.
rewrite big_ord_recr /=.
rewrite big_ord0.
rewrite add0r /=.
rewrite mxE /=.
rewrite mul0r.
rewrite add0r.
rewrite mxE.
rewrite /=.
rewrite mul1r.
rewrite /cofactor.
rewrite det_mx11.
rewrite mxE /=.
rewrite mxE /=.
rewrite mxE /=.
rewrite mulr1.
rewrite expr1.
by [].
Qed.

Lemma rotmx_det_3 : \det (rotmx 3) = 1.
Proof.
rewrite /rotmx.
repeat rewrite !(det_mx11, expand_det_col _ 0, big_ord_recr, big_ord0,
   mxE, mul0r, mulr0, add0r, addr0, mul1r, mulr1) /cofactor /=.
rewrite !exprS.
rewrite expr0.
rewrite mulr1.
rewrite mulrN.
rewrite mulr1.
rewrite opprK.
by [].
Qed.

Lemma rotmx_det n: \det (rotmx n.+1) = (-1) ^+ n.+2.
Proof.
rewrite (expand_det_col _ ord0).
(* The first column has shape 0
                              .
                              .
                              1 *)
rewrite (bigD1 ord_max) //=.
rewrite big1; last first.
  move=> i cndi; rewrite mxE /=.
  suff /negbTE -> : (i.+1 %% n.+1 != 0)%N.
    by rewrite mul0r.
  rewrite modn_small.
    by [].
  rewrite ltn_neqAle.
  rewrite ltn_ord.
  rewrite andbT.
  rewrite eqSS.
  rewrite -val_eqE /= in cndi.
  by [].
rewrite addr0.
have -> : rotmx n.+1 ord_max ord0 = 1.
(************************************)
  rewrite mxE.
  rewrite /=.
  by rewrite modnn.
rewrite mul1r /cofactor.
set m' := (X in \det X).
have -> : m' = 1%:M.
  apply/matrixP=> i j.
  rewrite !mxE.
  rewrite lift_max.
  rewrite modn_small. 
    by [].
  rewrite ltnS.
  by [].
rewrite det1 mulr1.
rewrite addn0 /=.
rewrite !exprS.
rewrite !mulN1r.
rewrite opprK.
by [].
Qed.

End sandbox.