proposition: Lemma proper_2_aux : Proper (SSP.Equal ==> eqop) SSP.choose.
proof: Proof. intros x y H. unfold eqop. case_eq (SSP.choose x); case_eq (SSP.choose y). intuition. intros HCN e HCS. apply SSP.choose_spec1 in HCS. apply SSP.choose_spec2 in HCN. rewrite H in HCS. apply SSPWEqP.MP.empty_is_empty_1 in HCN. rewrite HCN in HCS. apply SSPWEqP.MP.Dec.F.empty_iff in HCS. assumption. intros e HCS HCN. apply SSP.choose_spec1 in HCS. apply SSP.choose_spec2 in HCN. rewrite H in HCN. apply SSPWEqP.MP.empty_is_empty_1 in HCN. rewrite HCN in HCS. apply SSPWEqP.MP.Dec.F.empty_iff in HCS. assumption. intuition. Qed.
imports: Recdef NArith GeoCoq.Utils.sets