proposition: Lemma opposite_cons : forall d d1 r, opposite d d1 -> d1::d::r =r= r.
proof: Proof. intros d d1 r H;destruct d,d1;simpl ;try contradiction ; intro P;destruct P;simpl;auto; unfold translate;simpl; repeat f_equal;ring. Qed.
imports: List ZArith Bool Relations Setoid Morphisms RelationClasses EMonoid Lia