proposition: Lemma diagPlaneSurject : forall n : nat, let (i,j) := diagPlaneInv n in diagPlane i j = n.
proof: Proof. assert (forall i j:nat, let (k, l) := diagPlaneInvNext i j in diagPlane k l = S (diagPlane i j)). { intros. destruct (diagPlaneInvNext i j) as [k l] eqn:des. unfold diagPlane. unfold diagPlaneInvNext in des. destruct i. - inversion des. subst l. subst k. clear des. rewrite Nat.add_0_l. rewrite Nat.add_0_r. rewrite Nat.add_0_l. rewrite diagPlaneAbsNext. ring. - inversion des. subst l. subst k. clear des. assert ((i + S j) = S i + j)%nat. ring. rewrite H. assert (S j + (S i + j) * S (S i + j) / 2 = S (j + (S i + j) * S (S i + j) / 2))%nat. ring. rewrite H0. reflexivity. } induction n. - reflexivity. - unfold diagPlaneInv. simpl. unfold diagPlaneInv in IHn. destruct (iterateN2Func n 0 0 diagPlaneInvNext) as [i j]. rewrite <- IHn. apply H. Qed.
imports: QArith PeanoNat ArithRing ConstructiveReals ConstructiveAbs ConstructiveSum ConstructivePower ConstructiveLimits