complete!

affeldt-aist · Apr 25, 2024 · f6c7abf · f6c7abf
1 parent 9e6fb76
commit f6c7abf
Show file tree

Hide file tree

Showing 13 changed files with 231 additions and 232 deletions.
diff --git a/derive_matrix.v b/derive_matrix.v
@@ -362,7 +362,7 @@ Proof.
 transitivity ('d (crossmul (- v)) y); last first.
   by rewrite differential_cross_product spinN mx_lin1N.
 congr diff.
-by rewrite funeqE => /= u; rewrite (@lieC _ 'rV[R]_3) linearNl.
+by rewrite funeqE => /= u; rewrite (@lieC _ (vec3 R)) linearNl.
 Qed.
 
 End cross_product_matrix.

diff --git a/dh.v b/dh.v
@@ -75,7 +75,7 @@ Lemma normalized_plucker_positionP l :
 Proof.
 rewrite /normalized_plucker_position /normalized_plucker_direction -Line.vectorE.
 rewrite (linearZr_LR crossmul) /=.
-by rewrite dotmulvZ dotmulZv -dot_crossmulC (@liexx _ 'rV[T]_3) dotmulv0 2!mulr0.
+by rewrite dotmulvZ dotmulZv -dot_crossmulC (@liexx _ (vec3 T)) dotmulv0 2!mulr0.
 Qed.
 
 Definition normalized_plucker l : 'rV[T]_6 :=
@@ -119,14 +119,14 @@ Qed.
 
 Lemma plucker_eqn_self l : plucker_eqn \pt( l ) l = 0.
 Proof.
-rewrite /plucker_eqn -spinN -spinD spinE (@lieC _ 'rV[T]_3) addrC.
+rewrite /plucker_eqn -spinN -spinD spinE (@lieC _ (vec3 T)) addrC.
 by rewrite -linearBl /= subrr linear0l.
 Qed.
 
 Lemma in_plucker p l : p \in (l : pred _) -> plucker_eqn p l = 0.
 Proof.
 rewrite inE => /orP[/eqP ->|/andP[l0 H]]; first by rewrite plucker_eqn_self.
-rewrite /plucker_eqn -spinN -spinD spinE (@lieC _ 'rV[T]_3) addrC -linearBl.
+rewrite /plucker_eqn -spinN -spinD spinE (@lieC _ (vec3 T)) addrC -linearBl.
 apply/eqP.
 rewrite -/(colinear _ _) -colinearNv opprB colinear_sym.
 apply: (colinear_trans l0 _ H).
@@ -380,8 +380,14 @@ have H4 : From1To0 = dh_rot theta alpha.
     move: Hrot.
     rewrite H11 (eqP H21) H10 !mulNr opprK H20 -(mulrA (cos theta)) -expr2 mulrAC.
     rewrite -expr2 -opprD (mulrC (cos theta) (_ ^+ 2)) -mulrDl cos2Dsin2 mul1r.
-    rewrite mulrN -expr2 -mulrA mulrCA -expr2 -mulrA mulrCA -expr2 -mulrDr (addrC (_ ^+ 2)).
-    rewrite cos2Dsin2 mulr1 -expr2 sin2cos2 addrCA -opprD -mulr2n => /eqP.
+    rewrite [in LHS]mulrN -expr2.
+    rewrite mulrAC -expr2.
+    rewrite (mulrAC (cos alpha)) -expr2.
+    rewrite -mulrDl.
+    rewrite (addrC (_ ^+ 2)).
+    rewrite cos2Dsin2 mul1r.
+    rewrite -expr2.
+    rewrite (sin2cos2 theta) addrCA -opprD -mulr2n => /eqP.
     rewrite subr_eq addrC -subr_eq subrr eq_sym mulrn_eq0 /= sqrf_eq0 => ct0.
     rewrite {1}/From1To0 -lock H11 {1}/From1To0 -lock (eqP H21).
     by rewrite (eqP ct0) !(mulr0,mul0r) oppr0.
@@ -401,8 +407,9 @@ have H4 : From1To0 = dh_rot theta alpha.
     move: Hrot.
     rewrite H11 H21 H10 !mulNr opprK (eqP H20) -(mulrA (cos theta)) -expr2 mulrAC.
     rewrite -expr2 (mulrC (cos theta) (_ ^+ 2)) -mulrDl cos2Dsin2 mul1r.
-    rewrite mulNr mulrAC -!expr2 (mulrAC (cos alpha)) -expr2 -opprD -mulrDl.
-    rewrite (addrC _ (cos _ ^+ 2)) cos2Dsin2 mul1r mulrN -expr2 cos2sin2 -addrA -opprD.
+    rewrite mulNr mulrAC -2!expr2.
+    rewrite (mulrAC (cos alpha)) -expr2 -opprD -mulrDl.
+    rewrite (addrC (sin alpha ^+ 2)) cos2Dsin2 mul1r mulrN -expr2 cos2sin2 -addrA -opprD.
     rewrite -mulr2n => /eqP; rewrite subr_eq addrC -subr_eq subrr eq_sym mulrn_eq0 /=.
     rewrite sqrf_eq0 => /eqP st0.
     by rewrite st0 !(mulr0,oppr0) (mulrC (cos theta)).

diff --git a/differential_kinematics.v b/differential_kinematics.v
@@ -740,8 +740,6 @@ Hypothesis o4E : forall t, \o{Fmax t} = \o{Fim1 3%:R t} + d4 *: 'e_2.
 Lemma scale_realType (K : realType) (k1 : K) (k2 : K^o) : k1 *: k2 = k1 * k2.
 Proof. by []. Qed.
 
-Import rv3LieAlgebra.Exports.
-
 Lemma scara_geometric_jacobian t :
   derivable (theta1 : R^o -> R^o) t 1 ->
   derivable (theta2 : R^o -> R^o) t 1 ->
@@ -772,7 +770,7 @@ rewrite (mul_mx_row _ a) {}/a; congr (@row_mx _ _ 3 3 _ _).
   rewrite {1}o4E.
   rewrite linearDr /=.
   rewrite (linearZr_LR _ _ _ 'e_2)
-   /= {2}Hzvec (linearZl_LR _ _ _ 'e_2) /= liexx 2!{1}scaler0 addr0.
+   /= {2}Hzvec (linearZl_LR _ _ _ 'e_2) /= (@liexx _ (vec3 R)) 2!{1}scaler0 addr0.
   rewrite (_ : \o{Fmax t} - \o{Fim1 1 t} =
     (a2 * cos (theta1 t + theta2 t) *: 'e_0 +
     (a1 * sin (theta1 t) + a2 * sin (theta1 t + theta2 t) - a1 * sin (theta1 t)) *: 'e_1 +
@@ -784,16 +782,16 @@ rewrite (mul_mx_row _ a) {}/a; congr (@row_mx _ _ 3 3 _ _).
     rewrite addrC -[in RHS]addrA; congr (_ + _).
     by rewrite -addrA -scalerDl.
   rewrite linearDr /=.
-  rewrite (linearZr_LR _ _ _ 'e_2) /= (linearZl_LR (crossmul_bilinear _) 'e_2)
-          {2}(Hzvec t 1) /= liexx 2!{1}scaler0 addr0.
+  rewrite (linearZr_LR _ _ _ 'e_2) /= (linearZl_LR crossmul 'e_2)
+          {2}(Hzvec t 1) /= (@liexx _ (vec3 R)) 2!{1}scaler0 addr0.
   rewrite (addrC (a1 * sin _)) addrK.
   rewrite (_ : \o{Fmax t} - \o{Fim1 3%:R t} = d4 *: 'e_2%:R); last first.
     by rewrite o4E -addrA addrC subrK.
-  rewrite (linearZr_LR _ _ _ 'e_2) /= (linearZl_LR (crossmul_bilinear _) 'e_2)
-          {1}(Hzvec t 3%:R) /= liexx 2!scaler0 addr0.
+  rewrite (linearZr_LR _ _ _ 'e_2) /= (linearZl_LR crossmul 'e_2)
+          {1}(Hzvec t 3%:R) /= (@liexx _ (vec3 R)) 2!scaler0 addr0.
   rewrite o3E.
   rewrite linearDr /= (linearZr_LR _ _ _ 'e_2) (linearZl_LR _ 'e_2)
-          {2}(Hzvec t 0) /= liexx 2!scaler0 addr0.
+          {2}(Hzvec t 0) /= (@liexx _ (vec3 R)) 2!scaler0 addr0.
   rewrite {1}o2E {1}o1E.
   rewrite (_ : (fun _ => _) =
                 (a2 \*: (cos \o (theta2 + theta1) : R^o -> R^o)) +
@@ -806,8 +804,8 @@ rewrite (mul_mx_row _ a) {}/a; congr (@row_mx _ _ 3 3 _ _).
       exact: ex_derive.
       exact: H3.
     by rewrite deriveE // diff_cst add0r derive1E.
-  - rewrite !linearDr /= !(linearZr_LR (crossmul_bilinear _))
-            !(linearZl_LR (crossmul_bilinear _)) /= !Hzvec veckj vecki
+  - rewrite !linearDr /= !(linearZr_LR crossmul)
+            !(linearZl_LR crossmul) /= !Hzvec veckj vecki
             !{1}scalerN.
     rewrite -!addrA addrCA addrC -!addrA (addrCA (- _)) !addrA.
     rewrite -2!addrA [in RHS]addrC; congr (_ + _).

diff --git a/euclidean.v b/euclidean.v
@@ -1145,10 +1145,14 @@ Canonical crossmul_bilinear := [bilinear of (@crossmul R)].*)
 
 End crossmullie.
 
+Definition vec3 (R : comRingType) := 'rV[R]_3.
+
+HB.instance Definition _ R := GRing.Lmodule.on (vec3 R).
+
 Section rv3liealgebra.
 Variable R : comRingType.
 
-Let liexx (u : 'rV[R]_3) : u *v u = 0.
+Let liexx (u : vec3 R) : u *v u = 0.
 Proof.
 apply/rowP=> i.
 rewrite /crossmul; unlock.
@@ -1165,7 +1169,7 @@ by rewrite addrC dotmulC subrr.
 Qed.
 
 HB.instance Definition _ :=
-  @isLieAlgebra.Build R 'rV[R]_3 (@crossmul R : {bilinear 'rV_3 -> _ -> _}) liexx jacobi.
+  @isLieAlgebra.Build R (vec3 R) (@crossmul R : {bilinear (vec3 R) -> (vec3 R) -> (vec3 R)}) liexx jacobi.
 
 End rv3liealgebra.
 
@@ -1177,7 +1181,7 @@ Lemma mulmxl_crossmulr M u v : M *m (u *v v) = u *v (M *m v).
 Proof. by rewrite -(mul_rV_lin1 [linear of crossmul u]) mulmxA mul_rV_lin1. Qed.
 
 Lemma mulmxl_crossmull M u v : M *m (u *v v) = ((M *m u) *v v).
-Proof. by rewrite (@lieC _ 'rV[R]_3) mulmxN mulmxl_crossmulr -lieC. Qed.
+Proof. by rewrite (@lieC _ (vec3 R)) mulmxN mulmxl_crossmulr -(@lieC _ (vec3 R)). Qed.
 
 Lemma crossmul_triple u v w : u *d (v *v w) = \det (col_mx3 u v w).
 Proof.
@@ -1226,7 +1230,7 @@ Lemma dot_crossmulC u v x : u *d (v *v x) = (u *v v) *d x.
 Proof. by rewrite dotmul_crossmul_shift dotmulC. Qed.
 
 Lemma dot_crossmulCA u v w : u *d (v *v w) = - v *d (u *v w).
-Proof. by do 2 rewrite dot_crossmulC; rewrite linearNl (@lieC _ 'rV[R]_3)/=. Qed.
+Proof. by do 2 rewrite dot_crossmulC; rewrite linearNl (@lieC _ (vec3 R))/=. Qed.
 
 Lemma det_crossmul_dotmul M u v w :
   (\det M *: (u *v v)) *d w = (((u *m M) *v (v *m M)) *m M^T) *d w.
@@ -1242,7 +1246,7 @@ Proof. by apply/rowP=> i; rewrite -!dotmul_delta_mx det_crossmul_dotmul. Qed.
 
 Lemma dotmul_crossmul2 u v w : (u *v v) *v (u *v w) = (u *d (v *v w)) *: u.
 Proof.
-rewrite double_crossmul dot_crossmulC (dotmulC _ u) dot_crossmulC (@liexx _ 'rV[R]_3).
+rewrite double_crossmul dot_crossmulC (dotmulC _ u) dot_crossmulC (@liexx _ (vec3 R)).
 by rewrite dotmul0v scale0r subr0.
 Qed.
 
@@ -1270,7 +1274,7 @@ Lemma vece2 (i j : 'I_3) (k := - (i + j) : 'I_3) :
   'e_i *v 'e_j = (-1)^(perm3 i j)%N *+ (i != j) *: 'e_k :> 'rV[T]__.
 Proof.
 have [->|neq_ij] := altP (i =P j); rewrite (mulr0n,mulr1n).
-  by rewrite scale0r (@liexx _ 'rV[T]_3).
+  by rewrite scale0r (@liexx _ (vec3 T)).
 apply/rowP => k'; case: (I3P k' neq_ij); rewrite /crossmul; unlock; rewrite !mxE.
 - rewrite (@determinant_alternate _ _ _ 0 1) //=.
     by move: i j @k neq_ij => [[|[|[|?]]] ?] [[|[|[|?]]] ?] //=; rewrite mulr0.
@@ -1310,7 +1314,7 @@ Qed.
 Lemma common_normal_crossmul u v : (u *v v) _|_ u + v.
 Proof.
 rewrite normalmD ![(_ *v _) _|_ _]normal_sym crossmul_normal.
-by rewrite (@lieC _ 'rV[T]_3) normalmN crossmul_normal.
+by rewrite (@lieC _ (vec3 T)) normalmN crossmul_normal.
 Qed.
 
 End field_crossmul.
@@ -1579,7 +1583,7 @@ apply (iffP idP).
   rewrite rotationE; apply/andP; split.
     apply/orthogonal3P.
     rewrite ni nj /= zxy0 norm_crossmul_normal // xy0 !eqxx /= dot_crossmulC.
-    by rewrite liexx dotmul0v dot_crossmulCA liexx dotmulv0 !eqxx.
+    by rewrite (@liexx _ (vec3 T)) dotmul0v dot_crossmulCA (@liexx _ (vec3 T)) dotmulv0 !eqxx.
   rewrite -(col_mx3_row M) -crossmul_triple zxy0 double_crossmul dotmulvv nj expr1n.
   by rewrite scale1r (dotmulC (row 1 M)) xy0 scale0r subr0 dotmulvv ni expr1n.
 - move=> MSO; move: (MSO).

diff --git a/frame.v b/frame.v
@@ -173,7 +173,7 @@ Qed.
 Lemma noframe_posP : f~k = f~i *v f~j -> f~j = f~k *v f~i /\ f~i = f~j *v f~k.
 Proof.
 move=> ->; split.
-- rewrite (lieC _ f~i) /= double_crossmul idotj scale0r add0r opprK.
+- rewrite (@lieC _ (vec3 T) _ f~i) /= double_crossmul idotj scale0r add0r opprK.
   by rewrite dotmulvv noframe_norm expr1n scale1r.
 - rewrite double_crossmul dotmulvv noframe_norm expr1n scale1r dotmulC.
   by rewrite idotj scale0r subr0.
@@ -184,7 +184,7 @@ Proof.
 move=> ->; split.
 - rewrite linearNl /= linearNr /= double_crossmul dotmulvv.
   by rewrite noframe_norm expr1n scale1r idotj scale0r add0r opprK.
-- rewrite linearNl (@lieC _ 'rV[T]_3) linearNr opprK /= double_crossmul dotmulvv.
+- rewrite linearNl (@lieC _ (vec3 T)) linearNr opprK /= double_crossmul dotmulvv.
   by rewrite noframe_norm expr1n scale1r dotmulC idotj scale0r subr0.
 Qed.
 
@@ -227,29 +227,29 @@ Proof.
 move=> -> ->.
 rewrite !linearD /=.
 rewrite !linearZ /=.
-rewrite (lieC _ f~i).
-rewrite (lieC _ f~j).
-rewrite (lieC _ f~k).
+rewrite (@lieC _ (vec3 T) _ f~i).
+rewrite (@lieC _ (vec3 T) _ f~j).
+rewrite (@lieC _ (vec3 T) _ f~k).
 rewrite /=.
 rewrite ![in LHS]linearD /=.
-rewrite (_ : _ *v _ = 0); last by rewrite linearZ /= (@liexx _ 'rV[T]_3) scaler0.
+rewrite (_ : _ *v _ = 0); last by rewrite linearZ /= (@liexx _ (vec3 T)) scaler0.
 rewrite oppr0 scaler0 add0r.
 case: noframek => e3e1e2.
 - case: (noframe_posP e3e1e2) => Hj Hi.
   rewrite (_ : _ *v _ = v2 *: f~k); last by rewrite linearZ /= -e3e1e2.
   rewrite scalerN (_ : _ *v _ = - v3 *: f~j); last first.
-    by rewrite linearZ /= (@lieC _ 'rV[T]_3) /= -Hj scalerN scaleNr.
+    by rewrite linearZ /= (@lieC _ (vec3 T)) /= -Hj scalerN scaleNr.
   rewrite scaleNr opprK (_ : _ *v _ = - v1 *: f~k); last first.
-    by rewrite linearZ /= (@lieC _ 'rV[T]_3) e3e1e2 scalerN scaleNr.
+    by rewrite linearZ /= (@lieC _ (vec3 T)) e3e1e2 scalerN scaleNr.
   rewrite scaleNr opprK (_ : _ *v _ = 0); last first.
-    by rewrite linearZ /= (@liexx _ 'rV[T]_3) scaler0.
+    by rewrite linearZ /= (@liexx _ (vec3 T)) scaler0.
   rewrite scalerN scaler0 subr0.
   rewrite (_ : _ *v _ = v3 *: f~i); last by rewrite linearZ /= -Hi.
   rewrite scalerN (_ : _ *v _ = v1 *: f~j); last by rewrite linearZ /= Hj.
   rewrite scalerN (_ : _ *v _ = - v2 *: f~i); last first.
-    by rewrite linearZ /= (@lieC _ 'rV[T]_3) /= -Hi scaleNr scalerN.
+    by rewrite linearZ /= (@lieC _ (vec3 T)) /= -Hi scaleNr scalerN.
   rewrite scaleNr opprK (_ : _ *v _ = 0); last first.
-    by rewrite linearZ /= (@liexx _ 'rV[T]_3) scaler0.
+    by rewrite linearZ /= (@liexx _ (vec3 T)) scaler0.
   rewrite scalerN scaler0 subr0.
   move/esym : noframe_pos; rewrite e3e1e2 eqxx => /eqP ->.
   rewrite !scale1r -![in LHS]addrA addrC.
@@ -269,19 +269,19 @@ case: noframek => e3e1e2.
   rewrite (_ : _ *v _ = v3 *: f~j); last by rewrite linearZ /= -Hj.
   rewrite scalerN.
   rewrite (_ : _ *v _ = v1 *: f~k); last first.
-    by rewrite linearZ /= (@lieC _ 'rV[T]_3) -linearNl /= -e3e1e2.
+    by rewrite linearZ /= (@lieC _ (vec3 T)) -linearNl /= -e3e1e2.
   rewrite scalerN.
-  rewrite (_ : _ *v _ = 0); last by rewrite linearZ /= (@liexx _ 'rV[T]_3) scaler0.
+  rewrite (_ : _ *v _ = 0); last by rewrite linearZ /= (@liexx _ (vec3 T)) scaler0.
   rewrite oppr0 scaler0 addr0.
   rewrite (_ : _ *v _ = - v3 *: f~i); last first.
-    by rewrite linearZ /= (@lieC _ 'rV[T]_3) /= -Hi scalerN scaleNr.
+    by rewrite linearZ /= (@lieC _ (vec3 T)) /= -Hi scalerN scaleNr.
   rewrite scaleNr opprK.
   rewrite (_ : _ *v _ = - v1 *: f~j); last first.
-    by rewrite linearZ /= (@lieC _ 'rV[T]_3) /= -Hj scalerN scaleNr.
+    by rewrite linearZ /= (@lieC _ (vec3 T)) /= -Hj scalerN scaleNr.
   rewrite scaleNr opprK.
   rewrite (_ : _ *v _ = v2 *: f~i); last by rewrite linearZ /= -Hi.
   rewrite scalerN.
-  rewrite (_ : _ *v _ = 0); last by rewrite linearZ /= (@liexx _ 'rV[T]_3) scaler0.
+  rewrite (_ : _ *v _ = 0); last by rewrite linearZ /= (@liexx _ (vec3 T)) scaler0.
   rewrite oppr0 scaler0 addr0.
   move: noframe_neg; rewrite {1}e3e1e2 eqxx => /esym/eqP ->.
   rewrite -![in LHS]addrA addrC -addrA.
@@ -328,13 +328,13 @@ Lemma frame_icrossk : f~i *v f~k = - f~j.
 Proof. by move: (Frame.MSO f); rewrite !rowframeE => /SO_icrossk. Qed.
 
 Lemma frame_kcrossi : f~k *v f~i = f~j.
-Proof. by rewrite (@lieC _ 'rV[T]_3) /= frame_icrossk opprK. Qed.
+Proof. by rewrite (@lieC _ (vec3 T)) /= frame_icrossk opprK. Qed.
 
 Lemma frame_jcrossk : f~j *v f~k = f~i.
 Proof. by move: (Frame.MSO f); rewrite !rowframeE => /SO_jcrossk. Qed.
 
 Lemma frame_kcrossj : f~k *v f~j = - f~i.
-Proof. by rewrite (@lieC _ 'rV[T]_3) /= frame_jcrossk. Qed.
+Proof. by rewrite (@lieC _ (vec3 T)) /= frame_jcrossk. Qed.
 
 Definition frame_of_SO (M : 'M[T]_3) (HM : M \is 'SO[T]_3) : frame T :=
   @Frame.mk _ (NOFrame.mk (rotation_sub HM)) HM.
@@ -455,10 +455,10 @@ by rewrite dotmulZv dote2 mulr0.
 Qed.
 
 Lemma idotk : i *d k = 0.
-Proof. by rewrite /k dot_crossmulC (@liexx _ 'rV[T]_3) dotmul0v. Qed.
+Proof. by rewrite /k dot_crossmulC (@liexx _ (vec3 T)) dotmul0v. Qed.
 
 Lemma jdotk : j *d k = 0.
-Proof. by rewrite /k dot_crossmulCA (@liexx _ 'rV[T]_3) dotmulv0. Qed.
+Proof. by rewrite /k dot_crossmulCA (@liexx _ (vec3 T)) dotmulv0. Qed.
 
 Lemma normj : norm j = 1.
 Proof.
@@ -708,7 +708,7 @@ case: ifPn => [|_].
   by rewrite dotmulP dote2 scale_scalar_mx mulr0 mul_scalar_mx scale0r scaler0.
 apply/eqP.
 rewrite /normalize linearZr_LR -!scalemxAl scaler_eq0; apply/orP; right.
-rewrite /normalcomp/= linearD/= linearNr 2!linearZr_LR /= (@liexx _ 'rV[T]_3) 2!scaler0 subr0.
+rewrite /normalcomp/= linearD/= linearNr 2!linearZr_LR /= (@liexx _ (vec3 T)) 2!scaler0 subr0.
 move: (axialcompE (v *v 'e_0) v).
 rewrite v1 expr1n invr1 scale1r /i (negbTE (norm1_neq0 v1)) normalizeI // => <-.
 by rewrite axialcomp_crossmul.
@@ -971,10 +971,10 @@ Lemma idotj : i *d j = 0.
 Proof. by rewrite /= /i /j dotmulZv dotmulvZ dotmul_orthogonalize 2!mulr0. Qed.
 
 Lemma jdotk : j *d k = 0.
-Proof. by rewrite /k dot_crossmulCA liexx dotmulv0. Qed.
+Proof. by rewrite /k dot_crossmulCA (@liexx _ (vec3 T)) dotmulv0. Qed.
 
 Lemma idotk : i *d k = 0.
-Proof. by rewrite /k dot_crossmulC liexx dotmul0v. Qed.
+Proof. by rewrite /k dot_crossmulC (@liexx _ (vec3 T)) dotmul0v. Qed.
 
 Lemma normk : norm k = 1.
 Proof. by rewrite norm_crossmul_normal // ?normi // ?normj // idotj. Qed.
@@ -1038,15 +1038,15 @@ Qed.
 Lemma j_l_r : triad.j l1 l2 l3 *m rot_l2r = triad.j r1 r2 r3.
 Proof.
 rewrite /rot_l2r /= mulmxA mul_tr_col_mx3 dotmulC triad.idotj dotmulvv triad.normj //.
-rewrite expr1n dot_crossmulCA (@liexx _ 'rV[T]_3) dotmulv0 /matrix_of_noframe /=.
+rewrite expr1n dot_crossmulCA (@liexx _ (vec3 T)) dotmulv0 /matrix_of_noframe /=.
 rewrite col_mx3E row3E (mul_row_col 0%:M) mul_scalar_mx scale0r add0r.
 by rewrite (mul_row_col 1%:M) mul_scalar_mx scale1r mul_scalar_mx scale0r addr0.
 Qed.
 
 Lemma k_l_r : triad.k l1 l2 l3 *m rot_l2r = triad.k r1 r2 r3.
 Proof.
 rewrite /rot_l2r /= mulmxA mul_tr_col_mx3 {1}/triad.k dotmulC dot_crossmulC.
-rewrite (@liexx _ 'rV[T]_3) dotmul0v {1}/triad.k -dot_crossmulC (@liexx _ 'rV[T]_3) dotmulv0.
+rewrite (@liexx _ (vec3 T)) dotmul0v {1}/triad.k -dot_crossmulC (@liexx _ (vec3 T)) dotmulv0.
 rewrite /matrix_of_noframe /= dotmulvv triad.normk // expr1n col_mx3E row3E.
 do 2 rewrite (mul_row_col 0%:M) mul_scalar_mx scale0r add0r.
 by rewrite mul_scalar_mx scale1r.