proposition: Lemma move_translate : forall r P dx dy , move r (translate dx dy P) = translate dx dy (move r P).
proof: Proof. induction r as [|a r];simpl;[reflexivity|]. destruct a;simpl; intros;rewrite <- IHr;rewrite (translate_comm );auto. Qed.
imports: List ZArith Bool Relations Setoid Morphisms RelationClasses EMonoid Lia