construct lagP1

FEM/poly_Lagrange.v

@@ -31,9 +31,12 @@ Geometries using P2 or higher are left aside... *)
 
 Variable d : nat.
 
-Lemma lt_minus_1 : forall (j : 'I_(S d)), (j - 1 < d)%nat.
+Lemma lt_minus_1 : forall (j : 'I_(S d)), 
+  j <> ord0 -> (j - 1 < d)%nat.
 Proof.
-move => [j Hj] /=.
+move => [j Hj] H /=.
+
+lia.
 (* lia. does not work *)
 Admitted.
 
@@ -41,7 +44,7 @@ Admitted.
 Definition LagP1 : '('R^d -> R)^(S d) :=
   fun j x => match (eq_nat_dec j (@ord0 d)) with
     | left _ => 1 - (*comb_lin x (fun _ => 1)*) \big[+%R/0]_(i < d) (x i)
-    | right H => x (Ordinal (lt_minus_1 j))
+    | right H => x (Ordinal (lt_minus_1 j H))
     end.
 
 Definition vtxP1 : '('R^d)^(S d) :=
@@ -50,6 +53,12 @@ Definition vtxP1 : '('R^d)^(S d) :=
     | right H => kronecker (Ordinal (lt_minus_1 j)) i
     end.
 
+Definition vtxP1_aux : '('R^d)^(S d) :=
+  fun j i => match (eq_nat_dec j (@ord0 d)) with
+    | left _ => 0
+    | right H => kronecker (j - 1) i
+    end.
+
 Lemma LagP1_kron : forall i j,
   LagP1 j (vtxP1 i) = kronecker i j.
 Proof.