proposition: Lemma exists_grid : exists O E E' S U1 U2, ~ Col O E E' /\ Cs O E S U1 U2.
proof: Proof. destruct lower_dim_ex as [O [I [X HNC]]]. assert (H : ~ Col O I X) by auto; clear HNC; rename H into HNC. assert_diffs; destruct (ex_per_cong I O O X O I) as [J HJ]; Col; spliter. exists O; exists I; exists X; exists O; exists I; exists J. repeat (split; finish). Qed.
imports: GeoCoq.Tarski_dev.Ch15_lengths