Stream: Coq users

Topic: Two different data types


view this post on Zulip zohaze (Sep 01 2022 at 03:39):

n1*n2*n3<b /\ b1<=b2 ( All variables are of type nat).

I have two data types one for the multiplication of three numbers and second for esteblishing all possible relation between two variable. Want to ask how to link both data types to prpve above ?


Last updated: Feb 04 2023 at 21:02 UTC