proposition: Lemma double_pow_m1 (i: nat) (a : int): with_sgn i (with_sgn i a) = a.
proof: Proof. by rewrite mulrA -exprD -signr_odd addnn odd_double expr0 mul1r. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq choice fintype binomial) mathcomp(bigop ssralg poly ssrint) gaia(ssete7)