proposition: Lemma DiagTriangleShift : forall (p n : nat), let (i, j) := diagPlaneInv p in le (i + j) n -> le p (diagPlane 0 n).
proof: Proof. intros. destruct (diagPlaneInv p) as [i j] eqn:des. intros. apply (Nat.le_trans p (diagPlane 0 (i+j))). replace (diagPlane 0 (i + j)) with (p + i)%nat. rewrite <- (Nat.add_0_r p). rewrite <- Nat.add_assoc. apply Nat.add_le_mono_l. apply Nat.le_0_l. pose proof (diagPlaneSurject p). rewrite des in H0. unfold diagPlane in H0. unfold diagPlane. subst p. rewrite Nat.add_0_l. ring. unfold diagPlane. rewrite Nat.add_0_l. rewrite Nat.add_0_l. remember (i + j)%nat. apply Nat.add_le_mono. assumption. apply Nat.div_le_mono. auto. apply Nat.mul_le_mono_nonneg. apply Nat.le_0_l. assumption. apply Nat.le_0_l. apply le_n_S. assumption. Qed.
imports: QArith PeanoNat ArithRing ConstructiveReals ConstructiveAbs ConstructiveSum ConstructivePower ConstructiveLimits