proposition: Lemma sum_gaussD n : \sum_(0 <= i < n) i + \sum_(0 <= i < n) (n.-1 - i) = \sum_(0 <= i < n) n.-1.
proof: Proof. rewrite -big_split /=. apply: eq_big_nat => i Hi. rewrite addnC subnK //. by case: n Hi. Qed.
imports: mathcomp(all_ssreflect)