proposition: Lemma Cong_cases : forall 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 -> Cong A B C D.
proof: Proof. intros. decompose [or] H;clear H; Cong. Qed.
imports: GeoCoq.Tarski_dev.Definitions GeoCoq.Tactics.finish