math-comp / trajectories

0 stars 4 forks source link

finding an intersecting segment using b #29

Closed affeldt-aist closed 1 year ago

affeldt-aist commented 1 year ago

https://github.com/affeldt-aist/trajectories/blob/a0a147cf08c3f3a5eebef5a559c0487be241bcdf/theories/intersection.v#L205-L213

finding an intersecting segment using b instead of a <| sup I |> b

it should turn into a 10 lines proof

prove with "ivt for affine functions"

affeldt-aist commented 1 year ago

it was later observed that constructivity is maybe not a topic of interest here because deciding whether points are inside or outside is already decidable by checking whether a alternatively b is outside or inside the hull