proposition: Lemma from_Qpos_plus_homo (x y: Qpos) : from_Qpos (Qpos_plus x y) == from_Qpos x + from_Qpos y.
proof: Proof. reflexivity. Qed.
imports: CoRN.model.totalorder.QposMinMax Coq.Program.Program CoRN.model.structures.QposInf Coq.QArith.Qminmax