proposition: Lemma par_reflexivity : forall A B, A<>B -> Par A B A B.
proof: Proof. intros. unfold Par. unfold Par_strict. right. repeat split. assumption. assumption. apply col_trivial_1. apply col_trivial_3. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles