proposition: Lemma pick_lengths_ok_2 : forall s1 s2 ss, pick_lengths ss = Some(s1,s2) -> SSP.In s2 (SSP.remove s1 ss).
proof: Proof. intros s1 s2 ss H. unfold pick_lengths in H. case_eq (exists_witness (fun s : SSP.elt => match pick_lengths_aux s (SSP.remove s ss) with | Some _ => true | None => false end) ss). intros e1 HEW1. rewrite HEW1 in H. unfold pick_lengths_aux in H. case_eq (exists_witness (fun s2 : SSP.elt => negb (SP.is_empty (SP.inter e1 s2))) (SSP.remove e1 ss)). intros e2 HEW2. rewrite HEW2 in H. assert (HEq1 : e1 = s1) by (injection H; intros; assumption). rewrite HEq1 in *. assert (HEq2 : e2 = s2) by (injection H; intros; assumption). rewrite HEq2 in *. apply exists_witness_ok with (fun s2 : SSP.elt => negb (SP.is_empty (SP.inter s1 s2))). apply proper_1. assumption. intro HEW2. rewrite HEW2 in H. discriminate H. intro HEW. rewrite HEW in H. discriminate H. Qed.
imports: Recdef NArith GeoCoq.Utils.sets