Ends and outgoing germs of a single planar segment

Both end tags refer to the literal orientation from the first named point to the second.

theorem Cslib.Polygonal.Route.atEnd_line_iff (a b : ℂ) (i : Fin (line a b).segments) (t : ℝ) (side : Bool) : (line a b).AtEnd i t side ↔ t = if side = true then 1 else 0

A single segment reaches its tagged end exactly at the corresponding unit time.

theorem Cslib.Polygonal.Route.germ_line (a b : ℂ) (side : Bool) : (line a b).germ side = if side = true then a - b else b - a

The two outgoing germs of a single segment retain their opposite orientations.