proposition: Lemma find_segment_intersection t1 t2 x1 y1 xl1 yl1 x2 y2 xl2 yl2 : x1 <> 0 -> x2 * y1 - x1 * y2 <> 0 -> t1 * x1 + xl1 = t2 * x2 + xl2 -> t1 * y1 + yl1 = t2 * y2 + yl2 -> t1 * x1 + xl1 = (yl2 * x1 * x2 - yl1 * x1 * x2 - x1 * xl2 * y2 + xl1 * y1 * x2) / (y1 * x2 - x1 * y2).
proof: Proof. intros x1n0 dn0 eq1 eq2. assert (valt1 : t1 = (t2 * x2 + (xl2 - xl1)) / x1). enough (tmp : t1 = (t2 * x2 + xl2 - xl1) / x1) by now rewrite tmp; field. apply (Rmult_eq_reg_l x1); auto; apply (Rplus_eq_reg_r xl1). now rewrite (Rmult_comm x1 t1), eq1; field. revert eq2; rewrite valt1, Rdiv_plus_distr, Rmult_plus_distr_r. replace (t2 * x2 / x1 * y1 + (xl2 -xl1) / x1 * y1 + yl1) with ((t2 * x2 * y1 + (xl2 - xl1) * y1 + yl1 * x1) / x1) by now field. replace (t2 * y2 + yl2) with ((t2 * x1 * y2 + yl2 * x1) / x1) by now field. intros eq2; apply (Rmult_eq_reg_r (/x1)) in eq2;[|now apply Rinv_neq_0_compat]. apply (Rplus_eq_compat_r (- (t2 * x1 * y2))) in eq2. replace (t2 * x1 * y2 + yl2 * x1 + - (t2 * x1 * y2)) with (yl2 * x1) in eq2 by ring. replace (t2 * x2 * y1 + (xl2 - xl1) * y1 + yl1 * x1 + - (t2 * x1 * y2)) with (t2 * (x2 * y1 - x1 * y2) + (xl2 - xl1) * y1 + yl1 * x1) in eq2 by ring. apply (Rplus_eq_compat_r (- ((xl2 - xl1) * y1 + yl1 * x1))) in eq2. replace (t2 * (x2 * y1 - x1 * y2) + (xl2 - xl1) * y1 + yl1 * x1 + - ((xl2 - xl1) * y1 + yl1 * x1)) with (t2 * (x2 * y1 - x1 * y2)) in eq2 by ring. replace (yl2 * x1 + - ((xl2 - xl1) * y1 + yl1 * x1)) with ((yl2 - yl1) * x1 - (xl2 - xl1) * y1) in eq2 by ring. apply (Rmult_eq_compat_r (/ (x2 * y1 - x1 * y2))) in eq2. replace (t2 * (x2 * y1 - x1 * y2) * / (x2 * y1 - x1 * y2)) with t2 in eq2 by now field. rewrite eq2. field; split; auto; intros abs; case dn0; rewrite <- abs; ring. Qed.
imports: Arith QArith List smooth_trajectories Reals