Rename LagPd1_ref_kron_vtx -> LagPd1_ref_kron_vtxF.

Add LagPd1_ref_kron_vtx, LagPd1_ref_vtx_skipF.
Proof of Hface_ref_is_Ker.

FEM/geom_transf_affine.v

@@ -81,7 +81,7 @@ Qed.
 Lemma T_geom_vtx : forall i, T_geom (vtx_ref i) = vtx i.
 Proof.
 intro; unfold T_geom;
-    rewrite LagPd1_ref_kron_vtx baryc_ms_correct baryc_l_kron_r; easy.
+    rewrite LagPd1_ref_kron_vtxF baryc_ms_correct baryc_l_kron_r; easy.
 Qed.
 
 Lemma T_geom_vtxF : mapF T_geom vtx_ref = vtx.

FEM/poly_LagPd1.v

@@ -100,7 +100,7 @@ Proof. intros; apply LagPd1_ref_sum. Qed.
  #<A HREF="##RR9557v1">#[[RR9557v1]]#</A>#
  Lem 1554, Eq (9.45), p. 85. *)
 Lemma LagPd1_kron_vtx : forall i, LagPd1^~ (vtx i) = kronR i.
-Proof. intro; rewrite -LagPd1_ref_kron_vtx -(T_geom_inv_vtx Hvtx); easy. Qed.
+Proof. intro; rewrite -LagPd1_ref_kron_vtxF -(T_geom_inv_vtx Hvtx); easy. Qed.
 
 Lemma LagPd1_am : forall i, aff_map_ms (LagPd1 i).
 Proof.

FEM/poly_LagPd1_ref.v

@@ -207,7 +207,7 @@ Lemma LagPd1_ref_bc_gather : baryc_coord_ms vtx_ref = gather LagPd1_ref.
 Proof. rewrite LagPd1_ref_bc_scatter gather_scatter; easy. Qed.
 
 Lemma LagPd1_ref_barycF_rev :
-  forall (L : 'R^d.+1), sum L = 1 ->
+  forall {L : 'R^d.+1}, sum L = 1 ->
     LagPd1_ref^~ (barycenter_ms L vtx_ref) = L.
 Proof.
 intros; rewrite LagPd1_ref_bcF bc_ms_correct;
@@ -222,9 +222,18 @@ Qed.
 (**
  #<A HREF="##RR9557v1">#[[RR9557v1]]#</A>#
  Lem 1543, Eq (9.32), p. 81. *)
-Lemma LagPd1_ref_kron_vtx : forall i, LagPd1_ref^~ (vtx_ref i) = kronR i.
+Lemma LagPd1_ref_kron_vtxF : forall i, LagPd1_ref^~ (vtx_ref i) = kronR i.
 Proof. intro; rewrite LagPd1_ref_bcF; apply bc_kronF_r, vtx_ref_aff_indep. Qed.
 
+Lemma LagPd1_ref_kron_vtx : forall i j, LagPd1_ref j (vtx_ref i) = kronR i j.
+Proof. intros i j; move: j; apply extF_rev, LagPd1_ref_kron_vtxF. Qed.
+
+Lemma LagPd1_ref_vtx_skipF : forall i j, LagPd1_ref i (skipF vtx_ref i j) = 0.
+Proof.
+intros; unfold skipF; rewrite LagPd1_ref_kron_vtx.
+apply kron_is_0, ord_neq_compat, skip_ord_correct_m.
+Qed.
+
 Lemma LagPd1_ref_S_Monom :
   liftF_S LagPd1_ref = castF (pbinom_1_r d) (liftF_S (Monom_dk d 1)).
 Proof.
@@ -257,7 +266,7 @@ Qed.
 Lemma LagPd1_ref_lin_indep : lin_indep LagPd1_ref.
 Proof.
 intros L HL; extF; rewrite -lc_r_kron_r.
-rewrite -LagPd1_ref_kron_vtx -fct_lc_r_eq HL; easy.
+rewrite -LagPd1_ref_kron_vtxF -fct_lc_r_eq HL; easy.
 Qed.
 
 (**
@@ -274,7 +283,9 @@ Proof. apply (Dim _ _ _ LagPd1_ref_basis). Qed.
 
 Lemma LagPd1_ref_baryc_lc :
   forall L i, sum L = 1 -> LagPd1_ref i (lin_comb L vtx_ref) = L i.
-Proof. intros; rewrite -baryc_ms_eq// -{2}(LagPd1_ref_barycF_rev L); easy. Qed.
+Proof.
+move=>> HL; rewrite -baryc_ms_eq// -{2}(LagPd1_ref_barycF_rev HL); easy.
+Qed.
 
 Let K_geom_ref : 'R^d -> Prop := convex_envelop vtx_ref.
 
@@ -328,7 +339,18 @@ Definition Hface_ref (i : 'I_d.+1) : 'R^d -> Prop :=
  Lem 1564, p. 88. *)
 Lemma Hface_ref_is_Ker : forall i, Hface_ref i = Ker (LagPd1_ref i).
 Proof.
-Admitted.
+intro; unfold Hface_ref; apply subset_ext_equiv; split.
+(* *)
+intros _ [L HL]; apply (Ker_cas (LagPd1_ref_am _)); [easy |].
+intros j; rewrite Ker_equiv; apply LagPd1_ref_vtx_skipF.
+(* *)
+intros x_ref; move: (vtx_ref_aff_span x_ref) => /aff_span_EX [L [HL ->]].
+rewrite Ker_equiv.
+move: (LagPd1_ref_barycF_rev HL) => /extF_rev HL1; rewrite (HL1 i) => HLi.
+rewrite (baryc_skip_zero _ _ i)//; [apply Aff_span |].
+rewrite -(plus_zero_l (sum _)) -HLi -sum_skipF.
+1,2: apply invertible_eq_one; easy.
+Qed.
 
 Lemma Hface_ref_equiv :
   forall i x_ref, Hface_ref i x_ref <-> LagPd1_ref i x_ref = 0.