fact: Fixpoint make_broken_edges (e : edge) (break_points : seq Q) := match break_points with | nil => e :: nil | bp :: bps => let intermediate_point := (Bpt bp (pre_cross_second_coordinate e bp)) in Bedge (left_pt e) intermediate_point :: make_broken_edges (Bedge intermediate_point (right_pt e)) bps end.
imports: Arith QArith List smooth_trajectories Reals