proposition: Lemma translate_comm : forall dx dy dx' dy' P, translate dx dy (translate dx' dy' P) = translate dx' dy' (translate dx dy P).
proof: Proof. unfold translate; simpl; intros; f_equal; ring. Qed.
imports: List ZArith Bool Relations Setoid Morphisms RelationClasses EMonoid Lia