proposition: Lemma diagPlaneInject : forall i j : nat, diagPlaneInv (diagPlane i j) = pair i j.
proof: Proof. intros. destruct (diagPlaneInv (diagPlane i j)) as [k l] eqn:des. pose proof (diagPlaneSurject (diagPlane i j)). rewrite des in H. apply diagPlaneInjectBis in H. destruct H. subst k. subst l. reflexivity. Qed.
imports: QArith PeanoNat ArithRing ConstructiveReals ConstructiveAbs ConstructiveSum ConstructivePower ConstructiveLimits