proposition: Lemma proper_00 : forall s, Proper ((fun (t1 t2 : tST) => eqST t1 t2) ==> eq) (fun t : tST => pick_variety_aux s t).
proof: Proof. unfold pick_variety_aux, eqST. intros s t1 t2 HEq. case_eq (pick_variety_auxCP s t1); intro Ht1. { destruct (pick_variety_auxCP_forallT s t1) as [H1 H2]; clear H2. assert (H := H1 Ht1); clear H1; clear Ht1; rename H into Ht1. destruct (pick_variety_auxCP_forallT s t2) as [H1 H2]; clear H1. rewrite H2; try reflexivity; clear H2; intros p HIn; apply Ht1. clear Ht1; apply InCPOCP; apply InCPOCP in HIn. assert (H : eqList (CPToList (OCP t1)) (CPToList (OCP t2))). { assert (Ht1 := eqListSortOCP t1). assert (Ht2 := eqListSortOCP t2). apply eqListTrans with (PosSort.sort (CPToList t1)); try assumption. apply eqListTrans with (PosSort.sort (CPToList t2)); try assumption. apply eqListSym; assumption. } clear HEq; rename H into HEq; apply eqListOK in HEq. unfold InCP in *; rewrite HEq; auto. } { destruct (pick_variety_auxCP_existsF s t1) as [H1 H2]; clear H2. assert (H := H1 Ht1); clear H1; clear Ht1; rename H into Ht1. destruct (pick_variety_auxCP_existsF s t2) as [H1 H2]; clear H1. rewrite H2; try reflexivity; clear H2. destruct Ht1 as [p [HIn Hmem]]; exists p; split; auto. apply InCPOCP; apply InCPOCP in HIn. assert (H : eqList (CPToList (OCP t1)) (CPToList (OCP t2))). { assert (Ht1 := eqListSortOCP t1). assert (Ht2 := eqListSortOCP t2). apply eqListTrans with (PosSort.sort (CPToList t1)); try assumption. apply eqListTrans with (PosSort.sort (CPToList t2)); try assumption. apply eqListSym; assumption. } clear HEq; rename H into HEq; apply eqListOK in HEq. unfold InCP in *; rewrite <- HEq; auto. } Qed.
imports: Recdef NArith Sorting GeoCoq.Tactics.Coinc.Permutations GeoCoq.Utils.general_tactics GeoCoq.Utils.sets