fact: Definition h10c_to_h10sqcs (c : h10c) : list h10sqc := match c with | h10c_one x => [h10sqc_one (ζ x)] | h10c_plus x y z => [h10sqc_plus (ζ x) (ζ y) (ζ z)] | h10c_mult x y z => [ h10sqc_sq (ζ x) (θ x y 0); h10sqc_sq (ζ y) (θ x y 1); h10sqc_plus (θ x y 0) (θ x y 1) (θ x y 2); h10sqc_plus (ζ x) (ζ y) (θ x y 3); h10sqc_sq (θ x y 3) (θ x y 4); h10sqc_plus (ζ z) (ζ z) (θ x y 5); h10sqc_plus (θ x y 2) (θ x y 5) (θ x y 4)] end.
imports: List Lia Undecidability.DiophantineConstraints.H10C ssreflect ssrbool ssrfun