proposition: Lemma cop_sac2__sac : forall A B C D E F, Saccheri A B C D -> Saccheri A B E F -> D<>F -> Coplanar A B D F -> Saccheri D C E F.
proof: Proof. intros A B C D E F HSac HSac2 HDF HCop. assert(HPerp := sac__perp1214 _ _ _ _ HSac); assert(HPerp2 := sac__perp1214 _ _ _ _ HSac2). assert(HPerp3 := sac__perp3414 _ _ _ _ HSac); assert(HPerp4 := sac__perp3414 _ _ _ _ HSac2). assert(Col A D F). apply cop_perp2__col with A B; Perp. assert(Hdiff := sac_distincts _ _ _ _ HSac). assert(Hdiff2 := sac_distincts _ _ _ _ HSac2). unfold Saccheri in *; spliter; repeat split. - apply perp_per_1, perp_col0 with D A; Col; Perp. - apply perp_per_1, perp_sym, perp_col0 with F A; Col; Perp. - apply cong_transitivity with A B; Cong. - apply one_side_transitivity with B. apply col_one_side with A; Col; Side. apply invert_one_side, col_one_side with A; Col; Side. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.suma