search

affeldt-aist / coq-robot

Mathematics of Rigid Body Transformationss using Coq and MathComp
26 stars 2 forks source link

Lower the requirements of some definitions/lemmas #2

Closed drouhling closed 6 years ago

drouhling commented 6 years ago

I certainly missed some of them.

I also changed the statement of colinearP in order to prove it in a fieldType instead of a rcfType.