proposition: Lemma Cong_perm : forall A B C D, Cong A B C D -> Cong A B C D /\ Cong A B D C /\ Cong B A C D /\ Cong B A D C /\ Cong C D A B /\ Cong C D B A /\ Cong D C A B /\ Cong D C B A.
proof: Proof. intros. repeat split; Cong. Qed.
imports: GeoCoq.Tarski_dev.Definitions GeoCoq.Tactics.finish