• les types : PO (points) et PP (points pondérés et vecteurs)
• add_PP : PP->PP->PP (addition)
• mult_PP : R->PP->PP (multiplication par un réel)

• cons : R->PO->PP (constructeur de points pondérés)
• vec : PO->PO->PP (constructeur de vecteurs)

• axiomes pour formaliser l'espace vectoriel
  

les ressources de Coq utilisées

• les bibliothèques Reals et Fourier
• les tactiques Ring et Field pour simplifier les calculs

JFLA 2004 — F. GUILHOT