Preuve shape_fun_L_cur_eq

FEM/FE_LagP.v

@@ -682,40 +682,28 @@ rewrite -T_geom_transports_nodes; try easy; f_equal.
 unfold node_ref_aux; f_equal; apply ord_inj; easy.
 Qed.
 
+Lemma shape_fun_ext : forall (fe1 fe2:FE) (H:fe1 = fe2),
+   shape_fun fe1 = (castF (eq_sym (f_equal ndof H))
+    (mapF (castF_fun (eq_sym (f_equal d H))) (shape_fun fe2))).
+Proof.
+intros fe1 fe2 H; subst.
+apply extF; intros i; apply fun_ext; intros x.
+rewrite castF_refl.
+rewrite mapF_correct; unfold castF_fun; f_equal.
+now rewrite castF_refl.
+Qed.
+
 Lemma shape_fun_L_cur_eq : forall (vtx_cur :'R^{dL.+1,dL})
   (Hvtx : affine_independent vtx_cur),
   shape_fun (FE_LagPk_d_cur dL kL dL_pos kL_pos vtx_cur Hvtx) = 
     shape_fun_cur FE_LagPk_d_ref shape_Lag_ref vtx_cur Hvtx.
 Proof.
-intros vtx_cur Hvtx; unfold shape_fun_cur.
-apply extF; intros i.
-generalize (FE_cur_eq vtx_cur Hvtx); intros T.
-(*pose (t:= FE_LagPk_d_cur dL kL dL_pos kL_pos vtx_cur Hvtx); fold t in i, T |- *.
-assert (V : ndof t = ndof (FE_cur FE_LagPk_d_ref shape_Lag_ref vtx_cur Hvtx)) by easy.
-apply trans_eq with 
-  (shape_fun (FE_cur FE_LagPk_d_ref shape_Lag_ref vtx_cur Hvtx) 
-             (cast_ord V i)).
-subst t.
-generalize (eq_sym T); intros T'.*)
-
-
-(*apply is_local_shape_fun_inj.
-apply shape_fun_correct.
-generalize (shape_fun_correct  (FE_cur FE_LagPk_d_ref shape_Lag_ref vtx_cur Hvtx)).
-intros T.
-rewrite -FE_cur_eq in T.
-
-unfold is_local_shape_fun in *.
-
-rewrite -FE_cur_eq.
-
-apply shape_fun_correct.
-
-unfold FE_LagPk_d_ref.*)
-(*rewrite -> (FE_cur_eq vtx_cur Hvtx).
-apply shape_fun_correct.*)
-(*16/10/23: Ce n'est pas urgent *)
-Admitted.
+intros vtx_cur Hvtx; unfold shape_fun_cur; eapply trans_eq.
+apply shape_fun_ext with (H:=FE_cur_eq vtx_cur Hvtx).
+rewrite castF_id.
+apply extF; intros i; rewrite mapF_correct; apply fun_ext; intros x.
+unfold castF_fun; f_equal; now rewrite castF_id.
+Qed.
 
 (* From Aide-memoire EF Alexandre Ern : Eq 3.37 p. 63 *)
 (* "Ip (v o T) = (Ip v) o T" *)