Merge branch 'master' of depot.lipn.univ-paris13.fr:mayero/coq-num-analysis

FEM/FE_LagP.v

@@ -702,11 +702,12 @@ f_equal.
 apply T_geom_transports_nodes; easy.
 (* *)
 rewrite shape_fun_L_cur_eq.
-(* FIXME HM 19/02/24: pourquoi on ne peut pas utiliser 
-  shape_fun_cur_correct_rev ? *)
-erewrite shape_fun_cur_correct_rev2; easy.
+rewrite (shape_fun_cur_correct_rev FE_LagPk_d_ref _ vtx_cur); easy.
 Qed.
 
+
+
+
 End FE_Lagrange_ref_Pk_d_fact.
 
 (* Note du 4/7/23

FEM/FE_simplex.v

@@ -408,18 +408,12 @@ apply H2.
 Qed.
 
 Lemma shape_fun_cur_correct_rev : forall i : 'I_(ndof FE_cur), 
-  shape_fun_ref i = cur_to_ref (shape_fun_cur i).
+  shape_fun FE_ref i = cur_to_ref (shape_fun_cur i).
 Proof.
 intros i; rewrite shape_fun_cur_correct.
 apply cur_to_ref_comp. 
 Qed.
 
-Lemma shape_fun_cur_correct_rev2 :
-  shape_fun_ref = (fun i x_ref => shape_fun_cur i (T_geom vtx_cur x_ref)).
-Proof.
-apply extF; intros i.
-apply shape_fun_cur_correct_rev.
-Qed.
 
 Definition local_interp_cur : FRd d_cur -> FRd d_cur := 
   fun v => local_interp FE_cur v.