25 lines
685 B
Coq
25 lines
685 B
Coq
Record int_bipart : Set := {pneg : nat; ppos : nat}.
|
|
|
|
|
|
|
|
Notation "a !+ b" := (Peano.plus a b) (at level 50, left associativity).
|
|
Definition plus a b := Build_int_bipart
|
|
(pneg a !+ pneg b) (ppos a !+ ppos b).
|
|
Notation "a + b" := (plus a b).
|
|
|
|
Definition int_bipart_eq_part
|
|
: forall an bn, an = bn -> forall ap bp, ap = bp
|
|
-> Build_int_bipart an ap = Build_int_bipart bn bp.
|
|
Proof.
|
|
refine (fun _ _ eqn _ _ eqp => _).
|
|
refine (eq_ind _ (fun n => _ = Build_int_bipart n _) _ _ eqn).
|
|
refine (f_equal _ eqp).
|
|
Qed.
|
|
|
|
Require Import ArithRing.
|
|
|
|
Definition mult_comm : forall n m, n * m = m * n.
|
|
Proof.
|
|
refine (fun n m => int_bipart_eq_part _ _ _ _ _ _); simpl; ring.
|
|
Qed.
|