proposition: Lemma l12_9 : forall A1 A2 B1 B2 C1 C2, Coplanar C1 C2 A1 B1 -> Coplanar C1 C2 A1 B2 -> Coplanar C1 C2 A2 B1 -> Coplanar C1 C2 A2 B2 -> Perp A1 A2 C1 C2 -> Perp B1 B2 C1 C2 -> Par A1 A2 B1 B2.
proof: Proof. intros A1 A2 B1 B2 C1 C2. intros. unfold Par. unfold Par_strict. assert(A1 <> A2 /\ C1 <> C2) by (apply perp_distinct;assumption). assert(B1 <> B2 /\ C1 <> C2) by (apply perp_distinct;assumption). spliter. induction(col_dec A1 B1 B2). right. repeat split; auto. apply col_cop2_perp2__col with A1 C1 C2; auto. left. split. induction (perp_not_col2 C1 C2 A1 A2); Perp. apply coplanar_pseudo_trans with C1 C2 A1; Cop. apply coplanar_pseudo_trans with C1 C2 A2; Cop. intro. ex_and H10 AB. apply H9. induction(eq_dec_points AB A1). subst AB. assumption. assert(Perp A1 AB C1 C2) by (eauto using perp_col with col). apply col_cop2_perp2__col with AB C1 C2; Perp. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles