proposition: Fact Det22_morph : forall x, 〚 Det22 pX mX oppX x 〛= Det22 pY mY oppY (morph22 x).
proof: Proof. Proof using Hphi. destruct Hphi as [ G1 G2 G3 G4 G6 ]. intros (((?&?)&?)&?); simpl. rewrite G3, G6, G4, G4; auto. Qed.
imports: Arith ZArith Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime binomial sums)