proposition: Lemma valid_state_right s : valid_state s -> valid_state (rright s).
proof: Proof. case s; unfold valid_state, rright, fold_left; intros p1 p2 p3 p4 p5 p6 p7 o1 o2 o3 o4 o5 o6 o7 (H1, H2). split. - apply perm_trans with (1 := H1). refine (perm_trans _ _ _ (perm_swap _ _ _) _). apply perm_skip. refine (perm_trans _ _ _ (perm_swap _ _ _) _). refine (perm_trans _ _ _ _ (perm_swap _ _ _)). apply perm_skip. refine (perm_trans _ _ _ _ (perm_swap _ _ _)). apply perm_skip. refine (perm_trans _ _ _ _ (perm_swap _ _ _)). apply perm_id. - apply trans_equal with (2 := H2). apply eq_mod_3; auto; try (red; auto; fail). repeat rewrite oadd_mod_3 || rewrite oup_mod_3 || rewrite odown_mod_3. simpl. repeat rewrite Zmod_mod. do 7 match goal with |- ?X = _ => Zmod_plus_tac X end. do 7 match goal with |- _ = ?X => Zmod_plus_tac X end. apply f_equal2 with (f := BinIntDef.Z.modulo); auto. ring. Qed.
imports: ZArith List