fact: Definition Cong_5 P1 P2 P3 P4 P5 Q1 Q2 Q3 Q4 Q5 := Cong P1 P2 Q1 Q2 /\ Cong P1 P3 Q1 Q3 /\ Cong P1 P4 Q1 Q4 /\ Cong P1 P5 Q1 Q5 /\ Cong P2 P3 Q2 Q3 /\ Cong P2 P4 Q2 Q4 /\ Cong P2 P5 Q2 Q5 /\ Cong P3 P4 Q3 Q4 /\ Cong P3 P5 Q3 Q5 /\ Cong P4 P5 Q4 Q5.
imports: GeoCoq.Axioms.tarski_axioms