diff --git a/FEM/Compl/logic_compl.v b/FEM/Compl/logic_compl.v
index ff47a2338cfd234d2df8bff9a59ad16c978e4ebe..cbbab152eb8c37e82e127cf49e0323f9dc6d8a9b 100644
--- a/FEM/Compl/logic_compl.v
+++ b/FEM/Compl/logic_compl.v
@@ -321,3 +321,18 @@ rewrite not_ex_all_not_equiv; apply all_equiv;
 Qed.
 
 End Classical_predicate_Facts2.
+
+
+Section Datatypes_Facts.
+
+Context {T1 T2 : Type}.
+
+Lemma pair_neq_spec :
+  forall (a1 b1 : T1) (a2 b2 : T2),
+    (a1, a2) <> (b1, b2) <-> a1 <> b1 \/ a2 <> b2.
+Proof.
+intros; rewrite <- not_and_equiv, <- iff_not_equiv.
+apply pair_equal_spec.
+Qed.
+
+End Datatypes_Facts.
diff --git a/FEM/Compl/nat_compl.v b/FEM/Compl/nat_compl.v
index 1b028aa7f6f626b7fd5cb2b4696bdc35a663b737..36d2b845a9df7ef05a073d4d658e5e4986623db6 100644
--- a/FEM/Compl/nat_compl.v
+++ b/FEM/Compl/nat_compl.v
@@ -173,7 +173,7 @@ Qed.
 Lemma nat_ind2_strong :
   forall (P : nat -> nat -> Prop),
     (forall m n, (forall m1 n1, (m1 <= m)%coq_nat -> (n1 <= n)%coq_nat ->
-      (m1 + n1 < m + n)%coq_nat -> P m1 n1) -> P m n) ->
+      (m1, n1) <> (m, n) -> P m1 n1) -> P m n) ->
     forall m n, P m n.
 Proof.
 intros P HP; apply (strong_induction (fun m => forall n, P m n)); intros m Hm.
@@ -181,7 +181,7 @@ apply strong_induction; intros n Hn.
 apply HP; move=> m1 n1 /Nat.le_lteq Hm1 /Nat.le_lteq Hn1 H1.
 destruct Hm1; [apply Hm; easy |]; subst.
 destruct Hn1; [apply Hn; easy |]; subst.
-contradict H1; apply Nat.lt_irrefl.
+contradict H1; easy.
 Qed.
 
 Lemma nat_le_antisym_rev :
diff --git a/FEM/poly_Pdk.v b/FEM/poly_Pdk.v
index 5f3109f22ce8a86507d7df86c9cb46b4ab9e78fe..36518d7cc140e48e3611c372f11c6f501605a217 100644
--- a/FEM/poly_Pdk.v
+++ b/FEM/poly_Pdk.v
@@ -513,17 +513,20 @@ repeat apply: lin_span_plus_closed.
 (* . p1 q1 *)
 apply Pdk_widen.
 apply: (Hrec d n _ _ _ k.+1 l.+1); auto with arith.
+apply pair_neq_spec; left; easy.
 (* . *)
 replace n with ((n.-1).+1) by auto with zarith.
 apply Pdk_mul_var.
 apply: lin_span_plus_closed.
 (* . p1 q2*)
 apply: (Hrec d.+1 n.-1 _ _ _ k.+1 l); auto with arith.
+apply pair_neq_spec; right; auto with zarith.
 apply Pdk_widen; easy.
 apply le_S_n; apply Nat.le_trans with n; auto with zarith.
 apply Nat.le_trans with (2:=Hn); auto with arith.
 (* . p2 q1*)
 apply: (Hrec d.+1 n.-1 _ _ _ k l.+1); auto with arith.
+apply pair_neq_spec; right; auto with zarith.
 apply Pdk_widen; easy.
 apply le_S_n; apply Nat.le_trans with n; auto with zarith.
 (* . p2 * q2 *)
@@ -531,6 +534,7 @@ replace n with ((n.-2).+2) by auto with zarith.
 apply Pdk_mul_var.
 apply Pdk_mul_var.
 apply: (Hrec d.+1 n.-2 _ _ _ k l); auto with zarith arith.
+apply pair_neq_spec; right; auto with zarith.
 apply le_S_n, le_S_n; apply Nat.le_trans with n; auto with zarith.
 apply Nat.le_trans with (2:=Hn); apply PeanoNat.Nat.eq_le_incl.
 rewrite -PeanoNat.Nat.add_succ_r; auto with zarith arith.
diff --git a/Lebesgue/logic_compl.v b/Lebesgue/logic_compl.v
index da657abdc531e43b97d33c88f4d78ad8c4abd582..6f66b5fe83dfa18427178625900a9a0049eca7e4 100644
--- a/Lebesgue/logic_compl.v
+++ b/Lebesgue/logic_compl.v
@@ -36,4 +36,5 @@ Lemma iffrl {P} {Q} : P <-> Q -> Q -> P.
 Proof.
   now intros [_ QimpP].
 Qed.
+
 End LT.