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

# Conflicts:
#	FEM/FE_LagP.v

FEM/FE_LagP.v

@@ -397,7 +397,7 @@ End FE_LagPdk_from_ref.
 
 Section Face_unisolvence.
 
-(** Unisolvence for d>1 and k>0. *)
+(** Face unisolvence for d>1 and k>0. *)
 
 Context {d k : nat}.
 Hypothesis Hd : (1 < d)%coq_nat.
@@ -407,42 +407,15 @@ Hypothesis Hvtx : aff_indep_ms vtx.
 
 (**
  #<A HREF="##RR9557v1">#[[RR9557v1]]#</A>#
- Lem 1628, p. 107.#<BR>#
- Case i=0. *)
-Lemma Hface_0_unisolvence :
-  forall p, Pdk d k p ->
-    (forall (idk : 'I_(pbinom d k).+1),
-      Hface vtx ord0 (node vtx idk) -> p (node vtx idk) = 0) <->
-    (forall x, Hface vtx ord0 x -> p x = 0).
-Proof.
-assert (Hd0 : (0 < d)%coq_nat) by now apply Nat.lt_le_incl.
-intros p Hp; split; [| intros H idk Hidk; apply H; easy].
-intros H x Hx; destruct d as [| d1]; [easy |].
-assert (Hd1 : (0 < d1)%coq_nat) by now apply Nat.succ_lt_mono.
-rewrite -(f_invS_canS_r (T_geom_Hface_bijS Hvtx ord0) x)//.
-fold (T_geom_Hface_invS Hvtx ord0 x).
-pose (p0 := fun y => p (T_geom_Hface vtx ord0 y));
-  fold (p0 (T_geom_Hface_invS Hvtx ord0 x)).
-rewrite (unisolvence_inj_LagPSdSk Hd1 Hk _ vtx_ref_aff_indep p0)//.
-apply T_geom_Hface_comp; easy.
-extF idk; rewrite gather_eq; unfold Sigma_LagPSdSk, p0.
-rewrite -node_ref_node T_geom_Hface_0_node//.
-apply H, node_Hface_0; [easy.. |].
-rewrite Adk_inv_correct_r inj_CSdk_sum//.
-Qed.
-
-(**
- #<A HREF="##RR9557v1">#[[RR9557v1]]#</A>#
- Lem 1628, p. 107.#<BR>#
- Case i<>0. *)
-Lemma Hface_S_unisolvence :
-  forall {i} (Hi : i <> ord0) p, Pdk d k p ->
+ Lem 1628, p. 107. *)
+Lemma Hface_unisolvence :
+  forall {i} p, Pdk d k p ->
     (forall (idk : 'I_(pbinom d k).+1),
       Hface vtx i (node vtx idk) -> p (node vtx idk) = 0) <->
     (forall x, Hface vtx i x -> p x = 0).
 Proof.
 assert (Hd0 : (0 < d)%coq_nat) by now apply Nat.lt_le_incl.
-intros i Hi p Hp; split; [| move=> H idk Hidk; apply H; easy].
+intros i p Hp; split; [| move=> H idk Hidk; apply H; easy].
 intros H x Hx; destruct d as [| d1]; [easy |].
 assert (Hd1 : (0 < d1)%coq_nat) by now apply Nat.succ_lt_mono.
 rewrite -(f_invS_canS_r (T_geom_Hface_bijS Hvtx i) x)//.
@@ -451,9 +424,14 @@ pose (pi := fun y => p (T_geom_Hface vtx i y));
   fold (pi (T_geom_Hface_invS Hvtx i x)).
 rewrite (unisolvence_inj_LagPSdSk Hd1 Hk _ vtx_ref_aff_indep pi)//.
 apply T_geom_Hface_comp; easy.
-extF idk; rewrite gather_eq; unfold Sigma_LagPSdSk, pi.
-rewrite -node_ref_node T_geom_Hface_S_node//.
-apply H, (node_Hface_S Hvtx _ Hi Hd0 Hk); rewrite Adk_inv_correct_r;
+extF idk; rewrite gather_eq; unfold Sigma_LagPSdSk, pi; rewrite -node_ref_node.
+destruct (ord_eq_dec i ord0) as [-> | Hi].
+(* i = ord0 *)
+rewrite T_geom_Hface_0_node//; apply H, node_Hface_0; [easy.. |].
+rewrite Adk_inv_correct_r inj_CSdk_sum//.
+(* i <> ord0 *)
+rewrite T_geom_Hface_S_node//; apply H, (node_Hface_S Hvtx _ Hi Hd0 Hk).
+rewrite Adk_inv_correct_r;
     [apply insertF_correct_l; easy | rewrite inj_ASdki_sum; apply Adk_sum].
 Qed.