expand - Githubissues

math-comp / trajectories

0 stars 4 forks source link

expand #2

Closed affeldt-aist closed 2 years ago

affeldt-aist commented 2 years ago

https://github.com/affeldt-aist/trajectories/blob/d7eddd45c917c1d7e628d901bd494dd2253763a5/theories/ssr_descartes/bern.v#L106

Where is it defined? @ybertot

affeldt-aist commented 2 years ago

This is maybe the definition 24 of https://hal.inria.fr/inria-00503017v2/document.