proposition: Lemma lcos2_lcos : forall l1 l2 a b c, Eq_Lcos2 l1 a c l2 b c -> Eq_Lcos l1 a l2 b.
proof: Proof. intros. unfold Eq_Lcos2 in H. ex_and H lp. unfold Lcos2 in H. unfold Lcos2 in H0. ex_and H lx. ex_and H0 ly. unfold Eq_Lcos. assert(EqL lx ly). eapply(l13_6_bis lp _ _ c); auto. exists lx. split; auto. apply lcos_lg_anga in H. apply lcos_lg_anga in H0. spliter. rewrite H3;auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_4_cos GeoCoq.Tarski_dev.Annexes.project