proposition: Lemma diagPlaneInjectBis : forall i j k l : nat, diagPlane i j = diagPlane k l -> (i = k /\ j = l).
proof: Proof. intros. unfold diagPlane in H. remember (i + j)%nat as I. remember (k + l)%nat as K. assert (I = K). - destruct (Nat.lt_trichotomy I K). + exfalso. unfold lt in H0. assert ((S I) * S (S I) / 2 <= K * S K / 2)%nat. apply Nat.div_le_mono. intro absurd. inversion absurd. apply Nat.mul_le_mono_nonneg. apply Nat.le_0_l. assumption. apply Nat.le_0_l. apply le_n_S. assumption. rewrite diagPlaneAbsNext in H1. apply (Nat.add_le_mono_l (I * S I / 2 + S I) (K * S K / 2) l) in H1. rewrite <- H in H1. rewrite <- (Nat.add_comm (S I)) in H1. rewrite Nat.add_assoc in H1. apply Nat.le_le_add_le in H1. rewrite HeqI in H1. apply (Nat.nle_succ_diag_l j). apply (Nat.le_trans (S j) (l + S (i + j))). rewrite <- (Nat.add_0_r (S j)). assert (l + S (i + j) = S j + (l + i))%nat. ring. rewrite H2. pose proof (Nat.add_le_mono_l). apply Nat.add_le_mono_l. apply Nat.le_0_l. assumption. apply Nat.le_refl. + destruct H0. assumption. exfalso. unfold lt in H0. assert ((S K) * S (S K) / 2 <= I * S I / 2)%nat. apply Nat.div_le_mono. intro absurd. inversion absurd. apply Nat.mul_le_mono_nonneg. apply Nat.le_0_l. assumption. apply Nat.le_0_l. apply le_n_S. assumption. rewrite diagPlaneAbsNext in H1. apply (Nat.add_le_mono_l (K * S K / 2 + S K) (I * S I / 2) j) in H1. rewrite H in H1. rewrite <- (Nat.add_comm (S K)) in H1. rewrite Nat.add_assoc in H1. apply Nat.le_le_add_le in H1. rewrite HeqK in H1. apply (Nat.nle_succ_diag_l l). apply (Nat.le_trans (S l) (j + S (k + l))). rewrite <- (Nat.add_0_r (S l)). assert (j + S (k + l) = S l + (j + k))%nat. ring. rewrite H2. pose proof Nat.add_le_mono_l. apply Nat.add_le_mono_l. apply Nat.le_0_l. assumption. apply Nat.le_refl. - rewrite <- H0 in H. apply Nat.add_cancel_r in H. subst l. subst K. rewrite H0 in HeqI. apply Nat.add_cancel_r in HeqI. subst k. split; reflexivity. Qed.
imports: QArith PeanoNat ArithRing ConstructiveReals ConstructiveAbs ConstructiveSum ConstructivePower ConstructiveLimits