proposition: Theorem reduction : H10C_SAT ⪯ H10SQC_SAT.
proof: Proof. exists (fun cs => Argument.sqcs cs) => cs. constructor. - exact: Argument.transport. - exact: Argument.inverse_transport. Qed.
imports: List Lia Undecidability.DiophantineConstraints.H10C ssreflect ssrbool ssrfun Undecidability.Synthetic.Definitions