Commit 2023-01-13 13:23 1d0ad5a7

View on Github →

feat: port Data.PNat.Xgcd (#1408) Initial files generated by start_port.sh has been moved from Data/Pnat to Data/PNat.

Estimated changes

added def PNat.XgcdType.a
added def PNat.XgcdType.b
added theorem PNat.XgcdType.finish_v
added theorem PNat.XgcdType.flip_a
added theorem PNat.XgcdType.flip_b
added theorem PNat.XgcdType.flip_v
added theorem PNat.XgcdType.flip_w
added theorem PNat.XgcdType.flip_x
added theorem PNat.XgcdType.flip_y
added theorem PNat.XgcdType.flip_z
added def PNat.XgcdType.q
added def PNat.XgcdType.qp
added theorem PNat.XgcdType.qp_eq
added def PNat.XgcdType.r
added theorem PNat.XgcdType.reduce_a
added theorem PNat.XgcdType.reduce_b
added theorem PNat.XgcdType.reduce_v
added theorem PNat.XgcdType.rq_eq
added theorem PNat.XgcdType.start_v
added theorem PNat.XgcdType.step_v
added theorem PNat.XgcdType.step_wf
added def PNat.XgcdType.v
added def PNat.XgcdType.vp
added def PNat.XgcdType.w
added def PNat.XgcdType.z
added structure PNat.XgcdType
added def PNat.gcdA'
added theorem PNat.gcdA'_coe
added def PNat.gcdB'
added theorem PNat.gcdB'_coe
added def PNat.gcdD
added def PNat.gcdW
added def PNat.gcdX
added def PNat.gcdY
added def PNat.gcdZ
added theorem PNat.gcd_a_eq
added theorem PNat.gcd_b_eq
added theorem PNat.gcd_det_eq
added theorem PNat.gcd_eq
added theorem PNat.gcd_props
added theorem PNat.gcd_rel_left'
added theorem PNat.gcd_rel_left
added theorem PNat.gcd_rel_right'
added theorem PNat.gcd_rel_right
added def PNat.xgcd