proposition: Lemma diagPlaneAbsNext : forall n : nat, (S n * (S (S n)) / 2 = n * S n / 2 + S n)%nat.
proof: Proof. intro n. assert (S n * S (S n) = n * S n + S n * 2)%nat. ring. rewrite H. rewrite Nat.div_add. ring. intro absurd. inversion absurd. Qed.
imports: QArith PeanoNat ArithRing ConstructiveReals ConstructiveAbs ConstructiveSum ConstructivePower ConstructiveLimits