Add INR_invertible.

       inv_0 -> inv_zero,
       div_eq_one -> div_diag,
       mult_sum_distr_{l,r} -> mult_sum_{l,r}.
Add mult_plus_{l,r}, mult_opp_{l,r},
    is_inverse_one, is_inverse_eq_one, is_inverse_opp{,_rev,_equiv},
    inv_one, inv_opp, div_zero_l, div_one_{l,r}, div_eq_one_{l,r},
    div_plus, div_opp_{l,r}, div_minus, div_sum,
    scal_eq_R.

Rename node_face0_in_Cdk -> node_face_0_in_Cdk (modified),
       node_face0_in_Cdk_contra -> node_face_0_in_Cdk_contra,
       sub_node_out_face0 -> sub_node_out_face_0,
       node_faceSj_in_Adkj -> node_face_S_in_Adki,
       LagP1k_cur_decomp_P1k -> LagP1k_cur_ex_decomp_node.
Modify face_ref, face.
Add INR_eq_equiv, INR_0_equiv, node_ref_0_equiv,
    face_ref_eq.

Rename minus_zero_reg_sym -> minus_zero_sym_reg,
       minus_zero_reg_sym_contra -> minus_zero_sym_reg_contra.
Add minus_zero_sym_compat, minus_zero_sym_equiv,
    div_one_minus_equiv,
    scal_zero_r_equiv, one_minus_scal_inv_equiv.

Rename Pdk_am_comp_basis -> Pdk_lin_gen_comp (higher level),
       vtx_cur_node_cur_d1 -> vtx_node_cur_d1,
       vtx_ref_node_ref_d1 -> vtx_node_ref_d1,
       LagPd1_cur_n0 -> LagPd1_cur_S,
       Pd1_lin_span_LagPd1_cur -> LagPd1_cur_lin_gen,
       LagPd1_cur_decomp_Pd1_alt -> LagPd1_cur_ex_decomp_vtx,
       LagPd1_cur_decomp_Pd1 -> LagPd1_cur_ex_decomp_node.
Add node_vtx_cur_d1,
    LagPd1_cur_eq, LagPd1_ref_eq.

Modify lin_gen_ext, lin_gen_ext2.

Add am_equiv.
Mv temporary testing section from poly_Pdk to AffineSpace_aff_map.

Add node_cur_0k,
    Sigma_LagP0k_cur, Sigma_LagP0k_cur_lm, LagP0k_cur_unisolvence_inj.
Rename node_cur_d0 -> node_cur_Sd0,
       Sigma_LagPd0_cur -> Sigma_LagPSd0_cur,
       Sigma_LagPdSk_cur -> Sigma_LagPSdSk_cur,
       Sigma_LagPdk_cur -> Sigma_LagPSdk_cur,
       Sigma_LagPdk_cur_lm -> Sigma_LagPSdk_cur_lm,
       LagPd0_cur_unisolvence_inj -> LagPSd0_cur_unisolvence_inj,
       LagPd1_cur_unisolvence_inj -> LagPSd1_cur_unisolvence_inj,
       LagPdSk_cur_unisolvence_inj -> LagPSdSk_cur_unisolvence_inj,
       LagPdk_cur_unisolvence_inj -> LagPSdk_cur_unisolvence_inj,
       FE_LagPdk_cur -> FE_LagPSdk_cur,
       FE_LagPdk_ref -> FE_LagPSdk_ref,
       Sigma_LagPdk_cur_ref -> Sigma_LagPSdk_cur_ref,
       FE_ref_to_cur_LagPdk_ref_eq -> FE_ref_to_cur_LagPSdk_ref_eq,
       shape_fun_LagPdk_cur_eq -> shape_fun_LagPSdk_cur_eq,
       local_interp_LagPdk_comp -> local_interp_LagPSdk_comp.

Rename P0k_eq -> P0k_full (modified).
Unify proofs of Monom_0k_eq and Monom_d0_eq.
Cosmetics.

    hatSF_is_nonempty_equiv,
    skipF_1, skipF_one, skipF_singleF.

       full_fullset -> full_fullset_equiv.
Add empty_emptyset{,_rev}, full_fullset{,_rev}.
Rm useless full_fullset_alt.

       unisolvence_inj_LagPd0 -> LagPd0_cur_unisolvence_inj,
       unisolvence_inj_LagPd1_cur -> LagPd1_cur_unisolvence_inj,
       unisolvence_inj_LagP1k_cur -> LagP1k_cur_unisolvence_inj,
       unisolvence_inj_LagPdSk_cur -> LagPdSk_cur_unisolvence_inj,
       unisolvence_inj_LagPdk_cur -> LagPdk_cur_unisolvence_inj.

Make some arguments implicit.
Make beginning of FE_LagP closer to sections 8.2 and 8.3 of the paper.

Add possibility to test R_AffineSpace.

Use new defs from Binary_relation.
Rename ord_le_total -> ord_le_str_conn,
       ord_lt_total_strict -> ord_lt_conn.
Add ord_le_conn, ord_le_preorder, ord_le_partial_order, ord_le_total_order,
    ord_lt_strict_partial_order, ord_lt_strict_total_order.

Add aff_comb_Rms, barycenter_Rms, isobarycenter_Rms, middle_Rms, parallelogram_Rms.