Rename sub_nodeF -> sub_node_node,

       sub_nodeF_alt -> sub_nodeF.
Rm useless sub_node_ref_eq, T_geom_sub_nodeF.
The proof of sub_node_out_Hface_0 is now based on sub_node_ref_out_Hface_ref_0.

FEM/FE_LagP.v

@@ -199,7 +199,7 @@ rewrite Hq2 (IH2 q)//; [apply: mult_zero_r |]; intros iSdk.
 apply mult_reg_l with (LagPd1 Hvtx ord0 (sub_node k.+1 vtx iSdk)).
 apply invertible_equiv_R; rewrite -Hface_equiv;
     apply sub_node_out_Hface_0; easy.
-rewrite -(sub_nodeF k.+1) -fct_mult_eq -Hq2 sub_node_eq// Hp2 mult_zero_r; easy.
+rewrite -(sub_node_node k.+1) -fct_mult_eq -Hq2 sub_node_eq// Hp2 mult_zero_r//.
 Qed.
 
 (** Unisolvence result for d,k>0. *)

FEM/LagP_node.v

@@ -236,52 +236,19 @@ Variable vtx : 'R^{d.+1,d}.
 Definition sub_node (idk : [0..(pbinom d k.-1).+1)) : 'R^d :=
   T_geom vtx (sub_node_ref idk).
 
-Lemma sub_nodeF_alt : sub_node = mapF (T_geom vtx) sub_node_ref.
+Lemma sub_nodeF : sub_node = mapF (T_geom vtx) sub_node_ref.
 Proof. easy. Qed.
 
-Lemma sub_nodeF : sub_node = node (sub_vtx k vtx).
+Lemma sub_node_node : sub_node = node (sub_vtx k vtx).
 Proof.
-rewrite sub_nodeF_alt nodeF sub_vtxF -T_geom_comp mapF_comp.
+rewrite sub_nodeF nodeF sub_vtxF -T_geom_comp mapF_comp.
 f_equal.
 
 
 Admitted.
 
-(*
-Lemma sub_nodeF_alt : sub_node = mapF (T_geom (sub_vtx k vtx)) node_ref.
-Proof.
-rewrite sub_nodeF; extF; rewrite !mapF_correct.
-
-
- easy. Qed.
-*)
 End Sub_nodes_Def.
 
-(*
-Section Sub_nodes_ref_Facts1.
-
-Context {d k : nat}.
-Hypothesis Hk : (1 < k)%coq_nat.
-
-Lemma sub_node_ref_sub_node : sub_node k (@vtx_ref d) = node (sub_vtx_ref k).
-Proof. rewrite sub_vtx_refF; easy. Qed.
-
-(**
- #<A HREF="##RR9557v1">#[[RR9557v1]]#</A>#
- Lem 1598 (for [vtx_ref]), p. 100. *)
-Lemma sub_node_ref_eq :
-  sub_node k vtx_ref = widenF (pbinomS_monot_pred d k) (node vtx_ref).
-Proof.
-rewrite sub_node_ref; extF idk; unfold widenF; rewrite -node_ref_node.
-unfold node, sub_vtx_ref; rewrite T_geom_scal_ref//;
-    [| apply INR_ratio_invertible; easy].
-rewrite !node_ref_eqF scal_assoc div_eq mult_comm_R -mult_assoc mult_inv_r;
-    [| apply INR_pred_invertible; easy].
-rewrite mult_one_r; do 2 f_equal; apply Adk_previous_layer; easy.
-Qed.
-
-End Sub_nodes_ref_Facts1.
-*)
 
 Section Sub_nodes_Facts1.
 
@@ -289,14 +256,6 @@ Context {d k : nat}.
 Hypothesis Hk : (1 < k)%coq_nat.
 Variable vtx : 'R^{d.+1,d}.
 
-(*
-Lemma T_geom_sub_nodeF :
-  mapF (T_geom vtx) (sub_node k vtx_ref) = sub_node k vtx.
-Proof.
-rewrite !sub_nodeF -mapF_comp T_geom_comp -sub_vtx_refF sub_vtxF; easy.
-Qed.
-*)
-
 (**
  #<A HREF="##RR9557v1">#[[RR9557v1]]#</A>#
  Lem 1598, p. 100. *)
@@ -320,11 +279,8 @@ Lemma sub_node_out_Hface_0 :
   forall (idk : [0..(pbinom d k.-1).+1)),
     ~ Hface vtx ord0 (sub_node k vtx idk).
 Proof.
-(*intros idk H. apply (sub_node_ref_out_Hface_ref_0 ).*)
-
-assert (Hk0 : (0 < k)%coq_nat) by now apply Nat.lt_succ_l.
-intros; rewrite sub_node_eq// node_Hface_0// Adk_last_layer//.
-rewrite Nat.nle_gt; simpl; apply /ltP; easy.
+intro; rewrite -T_geom_Hface_eq// sub_nodeF mapF_correct Im_equiv;
+    [apply sub_node_ref_out_Hface_ref_0 | apply T_geom_inj]; easy.
 Qed.
 
 End Sub_nodes_Facts2.