structure IsMutation (X Y : Chromosome) : Prop

• le : X ≤ Y
• ne : X ≠ Y
• signature_eq : Chromosome.signature X = Chromosome.signature Y

theorem IsMutation.add_right {X Y : Chromosome} (Z : Chromosome) (h : IsMutation X Y) : IsMutation (X + Z) (Y + Z)

theorem IsMutation.of_add_right {X Y Z : Chromosome} (h : IsMutation (X + Z) (Y + Z)) : IsMutation X Y

theorem IsMutation.iff_add_right {X Y Z : Chromosome} : IsMutation (X + Z) (Y + Z) ↔ IsMutation X Y