proposition: Lemma par_distincts : forall A B C D, Par A B C D -> (Par A B C D /\ A <> B /\ C <> D).
proof: Proof. intros. split. assumption. unfold Par in H. induction H. assert_diffs. split; assumption. spliter. split; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles