proposition: Fact Det22_scal k : forall x, Det22 (M22scal k x) = (k ⊗ k) ⊗ Det22 x.
proof: Proof. Proof using R_is_ring. intros (((?,?),?),?); simpl; ring. Qed.
imports: Arith ZArith Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime binomial sums)