Add aff_indep_lin_indep{,_rev,_equiv},

    lin_indep_aff_indep{,_rev,_equiv}.

Algebra/Finite_dim/Finite_dim_AS_aff_indep.v

@@ -86,6 +86,37 @@ Proof.
 intros; split; [intros; apply aff_indep_all; easy | intros H; apply H].
 Qed.
 
+Lemma aff_indep_lin_indep :
+  forall {n} {A : 'E^n.+1} i0, lin_indep (frameF A i0) -> aff_indep A.
+Proof. move=> n A i0 /(aff_indep_any i0 ord0); easy. Qed.
+
+Lemma aff_indep_lin_indep_rev :
+  forall {n} {A : 'E^n.+1} i0, aff_indep A -> lin_indep (frameF A i0).
+Proof. move=>>; apply aff_indep_any. Qed.
+
+Lemma aff_indep_lin_indep_equiv :
+  forall {n} {A : 'E^n.+1} i0, aff_indep A <-> lin_indep (frameF A i0).
+Proof.
+intros; split; [apply aff_indep_lin_indep_rev | apply aff_indep_lin_indep].
+Qed.
+
+Lemma lin_indep_aff_indep_equiv :
+  forall {n} {u : 'V^n} (O : E) i0,
+    lin_indep u <-> aff_indep (inv_frameF O u i0).
+Proof.
+intros n u O i0. rewrite (aff_indep_lin_indep_equiv i0) frameF_inv_frameF//.
+Qed.
+
+Lemma lin_indep_aff_indep :
+  forall {n} {u : 'V^n} (O : E) i0,
+    aff_indep (inv_frameF O u i0) -> lin_indep u.
+Proof. move=>>; apply lin_indep_aff_indep_equiv. Qed.
+
+Lemma lin_indep_aff_indep_rev :
+  forall {n} {u : 'V^n} (O : E) i0,
+    lin_indep u -> aff_indep (inv_frameF O u i0).
+Proof. move=>>; apply lin_indep_aff_indep_equiv. Qed.
+
 Lemma aff_dep_any :
   forall {n} {A : 'E^n.+1} i0,
     (exists i, lin_dep (frameF A i)) -> lin_dep (frameF A i0).
@@ -119,7 +150,8 @@ Qed.
 Lemma aff_indep_decomp_uniq_rev :
   forall {n} {A : 'E^n.+1}, baryc_injL A -> aff_indep A.
 Proof.
-intros n A HA L HL.
+intros n A HA L HL; pose (L1 := part1F0 L).
+