proposition: Lemma not_ex_forall_not_7 : forall (T : Type) (P : T -> T -> T -> T -> T -> T -> T -> Prop), ~(exists x1 : T, exists x2 : T, exists x3 : T, exists x4 : T, exists x5 : T, exists x6 : T, exists x7 :T, P x1 x2 x3 x4 x5 x6 x7) <-> forall x1 : T, forall x2 : T, forall x3 : T, forall x4 : T, forall x5 : T, forall x6 : T, forall x7 : T, ~ P x1 x2 x3 x4 x5 x6 x7.
proof: Proof. intros; split; intro H1; intros; intro H2; [apply H1; exists x1, x2, x3, x4, x5, x6, x7; auto|]. destruct H2 as [x1 [x2 [x3 [x4 [x5 [x6 [x7 H2]]]]]]]. apply (H1 x1 x2 x3 x4 x5 x6 x7); auto. Qed.
imports: GeoCoq.Axioms.parallel_postulates GeoCoq.Tarski_dev.Ch12_parallel