proposition: Lemma all_imp_dist : forall (A:Type)(P Q:A->Prop), (forall x:A, P x -> Q x)-> (forall y:A, P y)-> forall z:A, Q z.
proof: Proof. intros A P Q H H0 z. apply H; apply H0; assumption. Qed.
imports: ZArith List Arith ZArithRing Relations Lia