proposition: Lemma zmon_pred_ok M j l : (zmon_pred j M) @@ (tail l) == (zmon j M) @@ l.
proof: Proof. destruct j; simpl; rewrite ?mkZmon_ok; simpl; rsimpl. - now rewrite Mjump_xO_tail. - rewrite Mjump_pred_double; rsimpl. Qed.
imports: Setoid Morphisms Env BinPos BinNat BinInt Ring_theory