proposition: Lemma refinement_resp_mult : forall m n Hm Hn, {k : nat | m = n * k} -> Refinement (Even_Partition Hab n Hn) (Even_Partition Hab m Hm).
proof: Proof. intros m n Hm Hn H. elim H; intros k Hk. red in |- *. cut (0 <> k); intro. exists (fun i : nat => i * k); repeat split. symmetry in |- *; assumption. intros. apply Nat.mul_lt_mono_pos_r. apply Nat.neq_0_lt_0; auto. assumption. intros. cut (i * k <= m). intro. exists H1. simpl in |- *. apply bin_op_wd_unfolded. algebra. generalize Hm; rewrite Hk. clear Hm; intro. rstepl (nring i[*]nring k[*] (b[-]a[/] _[//] mult_resp_ap_zero _ _ _ (nring_ap_zero' _ _ Hn) (nring_ap_zero' _ _ H0))). apply mult_wd. apply eq_symmetric_unfolded; apply nring_comm_mult. apply div_wd. algebra. apply eq_symmetric_unfolded; apply nring_comm_mult. rewrite Hk. apply Nat.mul_le_mono_r; assumption. apply Hm. rewrite Hk. rewrite <- H0. auto. Qed.
imports: CoRN.ftc.Continuity Coq(Lia)