proposition: Lemma variationC a b : variation a b = - variation b a.
proof: Proof. by rewrite /variation -!sgz_cp0 !sgzM; do 2?case: sgzP => _ //. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice path fintype) mathcomp(div bigop order ssralg poly polydiv ssrnum perm zmodp ssrint) mathcomp(polyorder polyrcf interval matrix mxtens)