proposition: Lemma det_conv (p p' q r : Plane) (t : R) : det (p <| t |> p') q r = (det p q r : R^o) <| t |> det p' q r.
proof: Proof. have sm t' u : t' *: (u : R^o) = t' * u by []. rewrite/conv !sm -det_cyclique -[det p q r]det_cyclique -[det p' q r]det_cyclique 3!det_scalar_productE -2!scalar_productZL -scalar_productDl; congr scalar_product. rewrite 2!scalerBr -!addrA; congr GRing.add. rewrite !addrA [-_ + _]addrC -addrA; congr GRing.add. by rewrite -[-(t*:r)]scaleNr -scalerBl -opprB opprK -addrA [-t+t]addrC subrr addr0 scaleN1r. Qed.
imports: mathcomp(all_ssreflect ssralg matrix ssrnum vector reals normedtype order boolp classical_sets) counterclockwise