Commit 5e3835f8 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Multiplications of fractions.

parent e1ec0f5a
Pipeline #2963 passed with stage
in 9 minutes and 48 seconds
......@@ -501,6 +501,8 @@ Next Obligation. by intros x y; apply Qcplus_pos_pos. Qed.
Definition Qp_minus (x y : Qp) : option Qp :=
let z := (x - y)%Qc in
match decide (0 < z)%Qc with left Hz => Some (mk_Qp z Hz) | _ => None end.
Program Definition Qp_mult (x y : Qp) : Qp := mk_Qp (x * y) _.
Next Obligation. intros x y. apply Qcmult_pos_pos; apply Qp_prf. Qed.
Program Definition Qp_div (x : Qp) (y : positive) : Qp := mk_Qp (x / ('y)%Z) _.
Next Obligation.
intros x y. assert (0 < ('y)%Z)%Qc.
......@@ -512,6 +514,7 @@ Qed.
Notation "1" := Qp_one : Qp_scope.
Infix "+" := Qp_plus : Qp_scope.
Infix "-" := Qp_minus : Qp_scope.
Infix "*" := Qp_mult : Qp_scope.
Infix "/" := Qp_div : Qp_scope.
Instance Qp_inhabited : Inhabited Qp := populate 1%Qp.
......@@ -535,6 +538,19 @@ Proof.
destruct (decide _) as [|[]]; auto. by f_equal; apply Qp_eq.
Qed.
Instance Qp_mult_assoc : Assoc (=) Qp_mult.
Proof. intros x y z; apply Qp_eq, Qcmult_assoc. Qed.
Instance Qp_mult_comm : Comm (=) Qp_mult.
Proof. intros x y; apply Qp_eq, Qcmult_comm. Qed.
Lemma Qp_mult_plus_distr_r x y z: (x * (y + z) = x * y + x * z)%Qp.
Proof. apply Qp_eq, Qcmult_plus_distr_r. Qed.
Lemma Qp_mult_plus_distr_l x y z: ((x + y) * z = x * z + y * z)%Qp.
Proof. apply Qp_eq, Qcmult_plus_distr_l. Qed.
Lemma Qp_mult_1_l x: (1 * x)%Qp = x.
Proof. apply Qp_eq, Qcmult_1_l. Qed.
Lemma Qp_mult_1_r x: (x * 1)%Qp = x.
Proof. apply Qp_eq, Qcmult_1_r. Qed.
Lemma Qp_div_1 x : (x / 1 = x)%Qp.
Proof.
apply Qp_eq; simpl.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment