proposition: Fact MI22_morph : forall x, morph22 (MI22 oppX x) = MI22 oppY (morph22 x).
proof: Proof. Proof using Hphi. destruct Hphi as [ G1 G2 G3 G4 G6 ]. do 1 intros (((?&?)&?)&?); apply M22_equal; repeat rewrite G3; repeat rewrite G4; auto. Qed.
imports: Arith ZArith Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime binomial sums)