proposition: Lemma even_partition_refinement : {N : nat | {HN : 0 <> N | Refinement P (Even_Partition Hab N HN) | Refinement Q (Even_Partition Hab N HN)}}.
proof: Proof. exists (m * n). cut (0 <> m * n); intro. exists H. unfold P in |- *; apply refinement_resp_mult. exists n; auto. unfold Q in |- *; apply refinement_resp_mult. exists m; auto with arith. clear P Q. cut (nring (R:=IR) (m * n) [#] [0]). rewrite <- H; simpl in |- *. apply ap_irreflexive_unfolded. astepl (nring m[*]nring (R:=IR) n). apply mult_resp_ap_zero; apply Greater_imp_ap; astepl (nring (R:=IR) 0); apply nring_less; apply Nat.neq_0_lt_0; auto. Qed.
imports: CoRN.ftc.Continuity Coq(Lia)