proposition: Lemma invariant_equiv st g1 g2 : refine g1 g2 -> refine g2 g1 -> invariant st g1 -> invariant st g2.
proof: Proof. move=> /refineP[Hs1 Hs2 Hg12] /refineP[_ _ Hg21] [H1 H2 H3 H4 [H5 H6]]. split => //. - move=> p Hv; rewrite -H3 //. by apply/idP/idP=> HH; [rewrite -Hg21 | rewrite -Hg12]. - move=> p1 p2 Hp1 Hp2 Hg1 Hg2. by rewrite Hg21 // Hg21 // H4 // -Hg21. split. move=> p1 p2 z Hp1 Hp2 Hz Hg1 Hin. by rewrite Hg21 // H5 // -Hg21. move=> p1 z1 Hp1 Hz1 Hg1 Hn. case: (H6 p1 z1) => //. by apply: contra Hg1 => Hgg1; rewrite -Hg12. move=> p2 [H1p2 H2p2 H3p2]. by exists p2; split=> //; rewrite -Hg12. Qed.
imports: mathcomp(all_ssreflect) mathcomp(zify)