Create a new file of bijectivity with all necessary lemmas.

ajouter des commentaires pour faciliter la lecture.
déplacer des morceaux en sandbox.

Rd = 'I_d -> R.
+ autres...

prove theta_shape_fun_local lemma.
Re-define the FE of reference.
Formalize elt_geom with bigop and 'I_n.
displace some parts to sandbox as we don't need them.

- Some cleaning in finite_element.v.

New version of ae_op_compat is now proved using the previous result.

This reverts commit 19ecefff.