proposition: Lemma null_root_ctrl_inc : (fun s : Site => ctrl_inc s (root_parent s0) (bm c0)) = (fun s : Site => 0%Z).
proof: Proof. apply funct_eq; intro. unfold ctrl_inc, card_mess in |- *; apply card_null. apply root_no_in_queue_inc. Qed.
imports: copy del rece_copy1 rece_copy2 rece_copy3 rece_dec rece_inc