proposition: Fact Det22_mult : forall x y, Det22 (x⊠y) = Det22 x ⊗ Det22 y.
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)