diff --git a/FEM/Algebra/Finite_family.v b/FEM/Algebra/Finite_family.v
index 7fdfd41f701ac21179216c0f4a21bca8550b8412..dc741fdd93641aa1585ca3b497cdc08858e0c410 100644
--- a/FEM/Algebra/Finite_family.v
+++ b/FEM/Algebra/Finite_family.v
@@ -4416,24 +4416,18 @@ contradict Hj1; move: Hj2; rewrite -!ord0_equiv_alt; move=>> ->.
 assert (HP0' : concatF P0 P' ord0) by easy.
 apply (filterP_ord_ind_l_in_0 HP0'), ord_inj; easy.
 (* *)
-pose (k := cast_ord (sym_eq (add1n _)) j).
-replace j with k by now apply ord_inj.
-assert (Hk1 : ~ (filterP_ord (cast_ord (eq_sym H) k) < 1)%coq_nat)
-  by now replace (cast_ord _ _) with (cast_ord (eq_sym H) j); [| apply ord_inj].
-assert (Hk2 : ~ (k < 1)%coq_nat) by easy.
-clear Hj1 Hj2.
 rewrite !concatF_correct_r; f_equal; apply ord_inj; simpl; apply addn_is_subn.
-assert (H0 : cast_ord (lenPF_ind_l_in HP0) (cast_ord (eq_sym H) k) <> ord0).
-  rewrite cast_ord_comp; contradict Hk2; apply cast_ord_0 in Hk2.
-  simpl in *; rewrite Hk2; apply Nat.lt_0_1.
+assert (H0 : cast_ord (lenPF_ind_l_in HP0) (cast_ord (eq_sym H) j) <> ord0).
+  rewrite cast_ord_comp; contradict Hj2; apply cast_ord_0 in Hj2.
+  simpl; rewrite Hj2; apply Nat.lt_0_1.
 rewrite filterP_ord_ind_l_in_n0 lift_S_correct -add1n; f_equal.
 assert (HP2 : equivFA (liftF_S (concatF P0 P')) (liftF_S P)).
   unfold P0, P'; rewrite concatF_splitF_S1p'.
   unfold castF_S1p; rewrite castF_refl; easy.
 rewrite (filterP_ord_ext HP2).
-assert (Hk : cast_ord (lenPF_ext HP2) (lower_S H0) = concat_r_ord Hk2)
+assert (Hj : cast_ord (lenPF_ext HP2) (lower_S H0) = concat_r_ord Hj2)
     by now apply ord_inj.
-rewrite Hk; easy.
+rewrite Hj; easy.
 Qed.
 
 Lemma filterPF_ind_l_out :