proposition: Lemma line_dec : forall B1 B2 C1 C2, (Col C1 B1 B2 /\ Col C2 B1 B2) \/ ~ (Col C1 B1 B2 /\ Col C2 B1 B2).
proof: Proof. intros. induction (col_dec C1 B1 B2); induction (col_dec C2 B1 B2);tauto. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles