proposition: Fact invmx_ctmat1 : invmx (map_mx (intr : int -> F) ctmat1) = \matrix_(i, j) (nth [::] [:: [:: 2%:R^-1; - 2%:R^-1; 0]; [:: 2%:R^-1; 2%:R^-1; -1]; [:: 0; 0; 1]] i)`_j :> 'M[F]_3.
proof: Proof. rewrite -[lhs in lhs = _]mul1r; apply: (canLR (mulrK _)). exact: ctmat1_unit. symmetry; rewrite /ctmat1. apply/matrixP => i j; rewrite !(big_ord_recl, big_ord0, mxE) /=. have halfP (K : numFieldType) : 2%:R^-1 + 2%:R^-1 = 1 :> K. by rewrite -mulr2n -[_ *+ 2]mulr_natl mulfV // pnatr_eq0. move: i; do ?[case=> //=]; move: j; do ?[case=> //=] => _ _; rewrite !(mulr1, mul1r, mulrN1, mulN1r, mulr0, mul0r, opprK); by rewrite !(addr0, add0r, oppr0, subrr, addrA, halfP). Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(finfun path matrix) mathcomp(bigop order ssralg poly polydiv ssrnum zmodp div ssrint) mathcomp(polyorder polyrcf interval polyXY) mathcomp(qe_rcf_th ordered_qelim mxtens)