proposition: Lemma Point_eqb_correct : forall p p', Point_eqb p p' = true <-> p = p'.
proof: Proof. destruct p;destruct p';simpl;split. - unfold Point_eqb; simpl; rewrite andb_true_iff; destruct 1. repeat rewrite <- Zeq_is_eq_bool in *. now rewrite H, H0. - injection 1;intros H0 H1;rewrite H0, H1; unfold Point_eqb; simpl; rewrite andb_true_iff;repeat rewrite <- Zeq_is_eq_bool; now split. Qed.
imports: List ZArith Bool Relations Setoid Morphisms RelationClasses EMonoid Lia