proposition: Lemma exists_square : forall A B, A<>B -> exists C D, Square A B C D.
proof: Proof. intros. destruct (exists_cong_per A B A B) as [C [HC1 HC2]]. assert_diffs. destruct (per__ex_saccheri B C A) as [D HSac]; Perp. exists C. exists D. assert (Rectangle B C D A) by (apply sac_rectangle;auto). unfold Square;split. eauto using rect_permut. Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec GeoCoq.Tarski_dev.Annexes.Tagged_predicates