[STATEMENT]
lemma desargues_config_2D_rkABPa_rkABPb_rkABPc :
  assumes "desargues_config_2D A B C A' B' C' P \<alpha> \<beta> \<gamma>" and "rk {A, B, C, A', B', C', P, Q} \<ge> 4" 
and "rk {P, Q, R} = 2" and "rk {P, R} = 2" and "rk {A', P} = 2" and "rk {B', P} = 2" and 
"rk {Q, A', a} = 2" and "rk {R, A, a} = 2" and "rk {Q, B', b} = 2" and "rk {R, B, b} = 2" and 
"rk {Q, C', c} = 2" and "rk {R, C, c} = 2"
  shows "rk {A, B, P, a} \<ge> 4" and "rk {A, B, P, b} \<ge> 4" and "rk {A, B, P, c} \<ge> 4"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 4 \<le> rk {A, B, P, a} &&& 4 \<le> rk {A, B, P, b} &&& 4 \<le> rk {A, B, P, c}
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. 4 \<le> rk {A, B, P, a}
 2. 4 \<le> rk {A, B, P, b}
 3. 4 \<le> rk {A, B, P, c}
[PROOF STEP]
have f1:"rk {A, B, C, A', B', C', P} = 3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rk {A, B, C, A', B', C', P} = 3
[PROOF STEP]
using assms(1) desargues_config_2D_def[of A B C A' B' C' P \<alpha> \<beta> \<gamma>] coplanar_ABCA'B'C'P
[PROOF STATE]
proof (prove)
using this:
desargues_config_2D A B C A' B' C' P \<alpha> \<beta> \<gamma>
desargues_config_2D A B C A' B' C' P \<alpha> \<beta> \<gamma> \<equiv> rk {A, B, C} = 3 \<and> rk {A', B', C'} = 3 \<and> rk {A, A', P} = 2 \<and> rk {B, B', P} = 2 \<and> rk {C, C', P} = 2 \<and> rk {A, B, \<gamma>} = 2 \<and> rk {A', B', \<gamma>} = 2 \<and> rk {A, C, \<beta>} = 2 \<and> rk {A', C', \<beta>} = 2 \<and> rk {B, C, \<alpha>} = 2 \<and> rk {B', C', \<alpha>} = 2 \<and> rk {A, B, C, A', B', C'} = 3 \<and> rk {A, B, P} = 3 \<and> rk {A, C, P} = 3 \<and> rk {B, C, P} = 3 \<and> rk {A, A'} = 2 \<and> rk {B, B'} = 2 \<and> rk {C, C'} = 2
\<lbrakk>rk {?A, ?A'} = 2; rk {?A, ?B, ?C, ?A', ?B', ?C'} = 3; rk {?A, ?A', ?P} = 2\<rbrakk> \<Longrightarrow> rk {?A, ?B, ?C, ?A', ?B', ?C', ?P} = 3

goal (1 subgoal):
 1. rk {A, B, C, A', B', C', P} = 3
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rk {A, B, C, A', B', C', P} = 3

goal (3 subgoals):
 1. 4 \<le> rk {A, B, P, a}
 2. 4 \<le> rk {A, B, P, b}
 3. 4 \<le> rk {A, B, P, c}
[PROOF STEP]
have f2:"rk {A', B', P, Q} = 4"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rk {A', B', P, Q} = 4
[PROOF STEP]
using assms(1) desargues_config_2D_def[of A B C A' B' C' P \<alpha> \<beta> \<gamma>] assms(2) assms(5) assms(6) 
      rk_A'B'PQ[of "A" "A'" "B" "C" "B'" "C'" "P" "Q"]
[PROOF STATE]
proof (prove)
using this:
desargues_config_2D A B C A' B' C' P \<alpha> \<beta> \<gamma>
desargues_config_2D A B C A' B' C' P \<alpha> \<beta> \<gamma> \<equiv> rk {A, B, C} = 3 \<and> rk {A', B', C'} = 3 \<and> rk {A, A', P} = 2 \<and> rk {B, B', P} = 2 \<and> rk {C, C', P} = 2 \<and> rk {A, B, \<gamma>} = 2 \<and> rk {A', B', \<gamma>} = 2 \<and> rk {A, C, \<beta>} = 2 \<and> rk {A', C', \<beta>} = 2 \<and> rk {B, C, \<alpha>} = 2 \<and> rk {B', C', \<alpha>} = 2 \<and> rk {A, B, C, A', B', C'} = 3 \<and> rk {A, B, P} = 3 \<and> rk {A, C, P} = 3 \<and> rk {B, C, P} = 3 \<and> rk {A, A'} = 2 \<and> rk {B, B'} = 2 \<and> rk {C, C'} = 2
4 \<le> rk {A, B, C, A', B', C', P, Q}
rk {A', P} = 2
rk {B', P} = 2
\<lbrakk>rk {A, A'} = 2; rk {A, B, C, A', B', C'} = 3; rk {A, A', P} = 2; rk {A, B, P} = 3; rk {B, B', P} = 2; rk {A', P} = 2; rk {B', P} = 2; 4 \<le> rk {A, B, C, A', B', C', P, Q}\<rbrakk> \<Longrightarrow> rk {A', B', P, Q} = 4

goal (1 subgoal):
 1. rk {A', B', P, Q} = 4
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rk {A', B', P, Q} = 4

goal (3 subgoals):
 1. 4 \<le> rk {A, B, P, a}
 2. 4 \<le> rk {A, B, P, b}
 3. 4 \<le> rk {A, B, P, c}
[PROOF STEP]
show "rk {A, B, P, a} \<ge> 4"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 4 \<le> rk {A, B, P, a}
[PROOF STEP]
using f1 f2 assms(1) desargues_config_2D_def[of A B C A' B' C' P \<alpha> \<beta> \<gamma>] assms(7) assms(2) assms(3) 
      assms(4) assms(8) rk_ABPa
[PROOF STATE]
proof (prove)
using this:
rk {A, B, C, A', B', C', P} = 3
rk {A', B', P, Q} = 4
desargues_config_2D A B C A' B' C' P \<alpha> \<beta> \<gamma>
desargues_config_2D A B C A' B' C' P \<alpha> \<beta> \<gamma> \<equiv> rk {A, B, C} = 3 \<and> rk {A', B', C'} = 3 \<and> rk {A, A', P} = 2 \<and> rk {B, B', P} = 2 \<and> rk {C, C', P} = 2 \<and> rk {A, B, \<gamma>} = 2 \<and> rk {A', B', \<gamma>} = 2 \<and> rk {A, C, \<beta>} = 2 \<and> rk {A', C', \<beta>} = 2 \<and> rk {B, C, \<alpha>} = 2 \<and> rk {B', C', \<alpha>} = 2 \<and> rk {A, B, C, A', B', C'} = 3 \<and> rk {A, B, P} = 3 \<and> rk {A, C, P} = 3 \<and> rk {B, C, P} = 3 \<and> rk {A, A'} = 2 \<and> rk {B, B'} = 2 \<and> rk {C, C'} = 2
rk {Q, A', a} = 2
4 \<le> rk {A, B, C, A', B', C', P, Q}
rk {P, Q, R} = 2
rk {P, R} = 2
rk {R, A, a} = 2
\<lbrakk>rk {?A, ?B, ?P} = 3; rk {?A, ?A'} = 2; rk {?A, ?A', ?P} = 2; rk {?Q, ?A', ?a} = 2; 4 \<le> rk {?A, ?B, ?C, ?A', ?B', ?C', ?P, ?Q}; rk {?A, ?B, ?C, ?A', ?B', ?C', ?P} = 3; rk {?P, ?Q, ?R} = 2; rk {?P, ?R} = 2; rk {?A', ?B', ?P, ?Q} = 4; rk {?R, ?A, ?a} = 2\<rbrakk> \<Longrightarrow> 4 \<le> rk {?A, ?B, ?P, ?a}

goal (1 subgoal):
 1. 4 \<le> rk {A, B, P, a}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
4 \<le> rk {A, B, P, a}

goal (2 subgoals):
 1. 4 \<le> rk {A, B, P, b}
 2. 4 \<le> rk {A, B, P, c}
[PROOF STEP]
show "rk {A, B, P, b} \<ge> 4"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 4 \<le> rk {A, B, P, b}
[PROOF STEP]
using f1 f2 assms(1) desargues_config_2D_def[of A B C A' B' C' P \<alpha> \<beta> \<gamma>] assms(9) assms(2) assms(3) 
      assms(4) assms(10) rk_ABPa[of "B" "A" "P" "B'" "Q" "b" "C" "A'" "C'" "R"]
[PROOF STATE]
proof (prove)
using this:
rk {A, B, C, A', B', C', P} = 3
rk {A', B', P, Q} = 4
desargues_config_2D A B C A' B' C' P \<alpha> \<beta> \<gamma>
desargues_config_2D A B C A' B' C' P \<alpha> \<beta> \<gamma> \<equiv> rk {A, B, C} = 3 \<and> rk {A', B', C'} = 3 \<and> rk {A, A', P} = 2 \<and> rk {B, B', P} = 2 \<and> rk {C, C', P} = 2 \<and> rk {A, B, \<gamma>} = 2 \<and> rk {A', B', \<gamma>} = 2 \<and> rk {A, C, \<beta>} = 2 \<and> rk {A', C', \<beta>} = 2 \<and> rk {B, C, \<alpha>} = 2 \<and> rk {B', C', \<alpha>} = 2 \<and> rk {A, B, C, A', B', C'} = 3 \<and> rk {A, B, P} = 3 \<and> rk {A, C, P} = 3 \<and> rk {B, C, P} = 3 \<and> rk {A, A'} = 2 \<and> rk {B, B'} = 2 \<and> rk {C, C'} = 2
rk {Q, B', b} = 2
4 \<le> rk {A, B, C, A', B', C', P, Q}
rk {P, Q, R} = 2
rk {P, R} = 2
rk {R, B, b} = 2
\<lbrakk>rk {B, A, P} = 3; rk {B, B'} = 2; rk {B, B', P} = 2; rk {Q, B', b} = 2; 4 \<le> rk {B, A, C, B', A', C', P, Q}; rk {B, A, C, B', A', C', P} = 3; rk {P, Q, R} = 2; rk {P, R} = 2; rk {B', A', P, Q} = 4; rk {R, B, b} = 2\<rbrakk> \<Longrightarrow> 4 \<le> rk {B, A, P, b}

goal (1 subgoal):
 1. 4 \<le> rk {A, B, P, b}
[PROOF STEP]
by (metis insert_commute)
[PROOF STATE]
proof (state)
this:
4 \<le> rk {A, B, P, b}

goal (1 subgoal):
 1. 4 \<le> rk {A, B, P, c}
[PROOF STEP]
show "rk {A, B, P, c} \<ge> 4"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 4 \<le> rk {A, B, P, c}
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 4 \<le> rk {A, B, P, c}
[PROOF STEP]
have f3:"rk {A, B, P, R, c} \<ge> 4"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 4 \<le> rk {A, B, P, R, c}
[PROOF STEP]
using rk_ABPRa[of A B P C A' B' C' Q R c] assms(1) desargues_config_2D_def[of A B C A' B' C' P \<alpha> \<beta> \<gamma>] 
        f1 assms(3) assms(4) f2
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>rk {A, B, P} = 3; rk {A, B, C, A', B', C', P} = 3; rk {P, Q, R} = 2; rk {P, R} = 2; rk {A', B', P, Q} = 4\<rbrakk> \<Longrightarrow> 4 \<le> rk {A, B, P, R, c}
desargues_config_2D A B C A' B' C' P \<alpha> \<beta> \<gamma>
desargues_config_2D A B C A' B' C' P \<alpha> \<beta> \<gamma> \<equiv> rk {A, B, C} = 3 \<and> rk {A', B', C'} = 3 \<and> rk {A, A', P} = 2 \<and> rk {B, B', P} = 2 \<and> rk {C, C', P} = 2 \<and> rk {A, B, \<gamma>} = 2 \<and> rk {A', B', \<gamma>} = 2 \<and> rk {A, C, \<beta>} = 2 \<and> rk {A', C', \<beta>} = 2 \<and> rk {B, C, \<alpha>} = 2 \<and> rk {B', C', \<alpha>} = 2 \<and> rk {A, B, C, A', B', C'} = 3 \<and> rk {A, B, P} = 3 \<and> rk {A, C, P} = 3 \<and> rk {B, C, P} = 3 \<and> rk {A, A'} = 2 \<and> rk {B, B'} = 2 \<and> rk {C, C'} = 2
rk {A, B, C, A', B', C', P} = 3
rk {P, Q, R} = 2
rk {P, R} = 2
rk {A', B', P, Q} = 4

goal (1 subgoal):
 1. 4 \<le> rk {A, B, P, R, c}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
4 \<le> rk {A, B, P, R, c}

goal (1 subgoal):
 1. 4 \<le> rk {A, B, P, c}
[PROOF STEP]
have "{A, B, P, R, c} \<subseteq> {A, B, C, P, R, c}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {A, B, P, R, c} \<subseteq> {A, B, C, P, R, c}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{A, B, P, R, c} \<subseteq> {A, B, C, P, R, c}

goal (1 subgoal):
 1. 4 \<le> rk {A, B, P, c}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
{A, B, P, R, c} \<subseteq> {A, B, C, P, R, c}
[PROOF STEP]
have f4:"rk {A, B, C, P, R, c} \<ge> 4"
[PROOF STATE]
proof (prove)
using this:
{A, B, P, R, c} \<subseteq> {A, B, C, P, R, c}

goal (1 subgoal):
 1. 4 \<le> rk {A, B, C, P, R, c}
[PROOF STEP]
using matroid_ax_2 f3
[PROOF STATE]
proof (prove)
using this:
{A, B, P, R, c} \<subseteq> {A, B, C, P, R, c}
?X \<subseteq> ?Y \<longrightarrow> rk ?X \<le> rk ?Y
4 \<le> rk {A, B, P, R, c}

goal (1 subgoal):
 1. 4 \<le> rk {A, B, C, P, R, c}
[PROOF STEP]
by (meson dual_order.trans)
[PROOF STATE]
proof (state)
this:
4 \<le> rk {A, B, C, P, R, c}

goal (1 subgoal):
 1. 4 \<le> rk {A, B, P, c}
[PROOF STEP]
have "rk {A, B, C, P, R, c} + rk {C, c} \<le> rk {A, B, C, P, c} + rk {R, C, c}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rk {A, B, C, P, R, c} + rk {C, c} \<le> rk {A, B, C, P, c} + rk {R, C, c}
[PROOF STEP]
using matroid_ax_3_alt[of "{C,c}" "{A, B, C, P, c}" "{R, C, c}"]
[PROOF STATE]
proof (prove)
using this:
{C, c} \<subseteq> {A, B, C, P, c} \<inter> {R, C, c} \<Longrightarrow> rk ({A, B, C, P, c} \<union> {R, C, c}) + rk {C, c} \<le> rk {A, B, C, P, c} + rk {R, C, c}

goal (1 subgoal):
 1. rk {A, B, C, P, R, c} + rk {C, c} \<le> rk {A, B, C, P, c} + rk {R, C, c}
[PROOF STEP]
by (simp add: insert_commute)
[PROOF STATE]
proof (state)
this:
rk {A, B, C, P, R, c} + rk {C, c} \<le> rk {A, B, C, P, c} + rk {R, C, c}

goal (1 subgoal):
 1. 4 \<le> rk {A, B, P, c}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
rk {A, B, C, P, R, c} + rk {C, c} \<le> rk {A, B, C, P, c} + rk {R, C, c}
[PROOF STEP]
have f5:"rk {A, B, C, P, c} \<ge> 4"
[PROOF STATE]
proof (prove)
using this:
rk {A, B, C, P, R, c} + rk {C, c} \<le> rk {A, B, C, P, c} + rk {R, C, c}

goal (1 subgoal):
 1. 4 \<le> rk {A, B, C, P, c}
[PROOF STEP]
using f4 assms(12) desargues_config_2D_rkAa_rkBb_rkCc assms(1) assms(9) assms(11) assms(2) assms(7)
[PROOF STATE]
proof (prove)
using this:
rk {A, B, C, P, R, c} + rk {C, c} \<le> rk {A, B, C, P, c} + rk {R, C, c}
4 \<le> rk {A, B, C, P, R, c}
rk {R, C, c} = 2
\<lbrakk>desargues_config_2D ?A ?B ?C ?A' ?B' ?C' ?P ?\<alpha> ?\<beta> ?\<gamma>; 4 \<le> rk {?A, ?B, ?C, ?A', ?B', ?C', ?P, ?Q}; rk {?Q, ?A', ?a} = 2; rk {?Q, ?B', ?b} = 2; rk {?Q, ?C', ?c} = 2\<rbrakk> \<Longrightarrow> rk {?A, ?a} = 2
\<lbrakk>desargues_config_2D ?A ?B ?C ?A' ?B' ?C' ?P ?\<alpha> ?\<beta> ?\<gamma>; 4 \<le> rk {?A, ?B, ?C, ?A', ?B', ?C', ?P, ?Q}; rk {?Q, ?A', ?a} = 2; rk {?Q, ?B', ?b} = 2; rk {?Q, ?C', ?c} = 2\<rbrakk> \<Longrightarrow> rk {?B, ?b} = 2
\<lbrakk>desargues_config_2D ?A ?B ?C ?A' ?B' ?C' ?P ?\<alpha> ?\<beta> ?\<gamma>; 4 \<le> rk {?A, ?B, ?C, ?A', ?B', ?C', ?P, ?Q}; rk {?Q, ?A', ?a} = 2; rk {?Q, ?B', ?b} = 2; rk {?Q, ?C', ?c} = 2\<rbrakk> \<Longrightarrow> rk {?C, ?c} = 2
desargues_config_2D A B C A' B' C' P \<alpha> \<beta> \<gamma>
rk {Q, B', b} = 2
rk {Q, C', c} = 2
4 \<le> rk {A, B, C, A', B', C', P, Q}
rk {Q, A', a} = 2

goal (1 subgoal):
 1. 4 \<le> rk {A, B, C, P, c}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
4 \<le> rk {A, B, C, P, c}

goal (1 subgoal):
 1. 4 \<le> rk {A, B, P, c}
[PROOF STEP]
have f6:"rk {A, B, C, P} \<le> 3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rk {A, B, C, P} \<le> 3
[PROOF STEP]
using matroid_ax_2 f1
[PROOF STATE]
proof (prove)
using this:
?X \<subseteq> ?Y \<longrightarrow> rk ?X \<le> rk ?Y
rk {A, B, C, A', B', C', P} = 3

goal (1 subgoal):
 1. rk {A, B, C, P} \<le> 3
[PROOF STEP]
by (smt insert_iff subsetI)
[PROOF STATE]
proof (state)
this:
rk {A, B, C, P} \<le> 3

goal (1 subgoal):
 1. 4 \<le> rk {A, B, P, c}
[PROOF STEP]
have "rk {A, B, C, P, c} + rk {A, B, P} \<le> rk {A, B, P, c} + rk {A, B, C, P}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rk {A, B, C, P, c} + rk {A, B, P} \<le> rk {A, B, P, c} + rk {A, B, C, P}
[PROOF STEP]
using matroid_ax_3_alt[of "{A, B, P}" "{A, B, P, c}" "{A, B, C, P}"]
[PROOF STATE]
proof (prove)
using this:
{A, B, P} \<subseteq> {A, B, P, c} \<inter> {A, B, C, P} \<Longrightarrow> rk ({A, B, P, c} \<union> {A, B, C, P}) + rk {A, B, P} \<le> rk {A, B, P, c} + rk {A, B, C, P}

goal (1 subgoal):
 1. rk {A, B, C, P, c} + rk {A, B, P} \<le> rk {A, B, P, c} + rk {A, B, C, P}
[PROOF STEP]
by (simp add: insert_commute)
[PROOF STATE]
proof (state)
this:
rk {A, B, C, P, c} + rk {A, B, P} \<le> rk {A, B, P, c} + rk {A, B, C, P}

goal (1 subgoal):
 1. 4 \<le> rk {A, B, P, c}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
rk {A, B, C, P, c} + rk {A, B, P} \<le> rk {A, B, P, c} + rk {A, B, C, P}
[PROOF STEP]
have "rk {A, B, P, c} \<ge> rk {A, B, C, P, c}"
[PROOF STATE]
proof (prove)
using this:
rk {A, B, C, P, c} + rk {A, B, P} \<le> rk {A, B, P, c} + rk {A, B, C, P}

goal (1 subgoal):
 1. rk {A, B, C, P, c} \<le> rk {A, B, P, c}
[PROOF STEP]
using assms(1) desargues_config_2D_def[of A B C A' B' C' P \<alpha> \<beta> \<gamma>] f6
[PROOF STATE]
proof (prove)
using this:
rk {A, B, C, P, c} + rk {A, B, P} \<le> rk {A, B, P, c} + rk {A, B, C, P}
desargues_config_2D A B C A' B' C' P \<alpha> \<beta> \<gamma>
desargues_config_2D A B C A' B' C' P \<alpha> \<beta> \<gamma> \<equiv> rk {A, B, C} = 3 \<and> rk {A', B', C'} = 3 \<and> rk {A, A', P} = 2 \<and> rk {B, B', P} = 2 \<and> rk {C, C', P} = 2 \<and> rk {A, B, \<gamma>} = 2 \<and> rk {A', B', \<gamma>} = 2 \<and> rk {A, C, \<beta>} = 2 \<and> rk {A', C', \<beta>} = 2 \<and> rk {B, C, \<alpha>} = 2 \<and> rk {B', C', \<alpha>} = 2 \<and> rk {A, B, C, A', B', C'} = 3 \<and> rk {A, B, P} = 3 \<and> rk {A, C, P} = 3 \<and> rk {B, C, P} = 3 \<and> rk {A, A'} = 2 \<and> rk {B, B'} = 2 \<and> rk {C, C'} = 2
rk {A, B, C, P} \<le> 3

goal (1 subgoal):
 1. rk {A, B, C, P, c} \<le> rk {A, B, P, c}
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
rk {A, B, C, P, c} \<le> rk {A, B, P, c}

goal (1 subgoal):
 1. 4 \<le> rk {A, B, P, c}
[PROOF STEP]
thus "rk {A, B, P, c} \<ge> 4"
[PROOF STATE]
proof (prove)
using this:
rk {A, B, C, P, c} \<le> rk {A, B, P, c}

goal (1 subgoal):
 1. 4 \<le> rk {A, B, P, c}
[PROOF STEP]
using f5
[PROOF STATE]
proof (prove)
using this:
rk {A, B, C, P, c} \<le> rk {A, B, P, c}
4 \<le> rk {A, B, C, P, c}

goal (1 subgoal):
 1. 4 \<le> rk {A, B, P, c}
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
4 \<le> rk {A, B, P, c}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
4 \<le> rk {A, B, P, c}

goal:
No subgoals!
[PROOF STEP]
qed