proposition: Fact Diag22_expo n x y : expo22 n (x,z,z,y) = (expoR n x,Rzero,Rzero,expoR n y).
proof: Proof. Proof using R_is_ring. induction n as [ | n IHn ]; try (simpl; auto; fail). do 3 rewrite mscal_S; rewrite IHn. apply M22_equal; ring. Qed.
imports: Arith ZArith Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime binomial sums)