[coq] [mathcomp] add few mathcomp egs

coq/mathcomp/bigop-egs.v

@@ -0,0 +1,5 @@
+From mathcomp Require Import all_ssreflect all_algebra.
+
+Lemma sum_odd_3: \sum_(0 <= i < 3.*2 | odd i) i = 3^2.
+Proof.  by rewrite unlock /=. Qed.
+

coq/mathcomp/general.v

@@ -0,0 +1,10 @@
+From mathcomp Require Import all_ssreflect.
+
+(** * Using [exists] *)
+Goal forall w:seq nat,
+    (exists w1 w2: seq nat, w = (w1 ++ w2)%list /\ (length w)==0%nat) -> w = [::].
+Proof.
+    move=> w [w1 [w2]].
+      by case; case: w; case: w1; case: w2.
+Qed.
+

coq/mathcomp/matrix-egs.v

@@ -0,0 +1,24 @@
+From mathcomp Require Import all_ssreflect all_algebra.
+
+Open Scope ring_scope.
+
+(* https://coq.zulipchat.com/#narrow/stream/237664-math-comp-users/topic/A.20matrix.20mul.20proof *)
+Goal
+  let mt: 'M[bool]_(2,3) :=
+    \matrix_(i<2, j<3) (if i == 0 && (j == 1) :> nat then 1 else 0) in
+  let rw := (\row_i (if i == 0 then 1 else 0)) *m mt in
+  (\sum_j (rw 0 j)) == 1.
+Proof.
+  rewrite //=.
+  by do ![rewrite !big_ord_recl !big_ord0 !mxE].
+Qed.
+
+Lemma constMxElem {V: Type} (rows cols: nat) (v: V):
+  forall (i: 'I_rows) (j: 'I_cols),
+    (((const_mx v):'M_(rows, cols)) i j) = v.
+Proof.
+  move=> i j.
+  rewrite /const_mx unlock.
+  rewrite /fun_of_matrix /=.
+  by rewrite ffunE.
+Qed.