proposition: Lemma Rectangle_triv : forall A B, A<>B -> Rectangle A A B B.
proof: Proof. intros. unfold Rectangle. split;Cong. unfold Plg. split. intuition. elim (midpoint_existence A B). intros. exists x. tauto. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel