proposition: Lemma congr_variation a b a' b' : sgz a = sgz a' -> sgz b = sgz b' -> variation a b = variation a' b'.
proof: Proof. by rewrite /variation -!sgz_cp0 !sgzM => -> ->. 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)